Discussion:
Refuting Incompleteness and Undefinability Version(15)
Add Reply
peteolcott
2018-11-05 19:58:19 UTC
Reply
Permalink
A world class expert provided some coaching. They have published very much in the field of Incompleteness and many related fields.

They changed my formulation of a correct simplification of Gödel's 1931 Incompleteness Theorem: ∀F ∈ Formal_Systems (∃G ∈ F (G ↔ ∃Γ ⊆ F ~(Γ ⊢ G)))

into this:
L(F) means the language of formal system F.
∀F (F ∈ Formal_Systems & Q ⊆ F) → ∃G ∈ L(F) (G ↔ ~(F ⊢ G))
Q here is Robinson Arithmetic (the theorem fails for some weaker formal systems)

On 11/5/2018 9:53 AM, exflaso.quodlibet wrote:
Because of above referenced feedback I now paraphrased it to this:
∀F ⊇ Q (∃G ∈ L(F) (G ↔ ~(F ⊢ G)))

As long as any simplification of the original theorem sufficiently captures the essence of the original theorem, any refutation of this simplification applies equally to the original theorem by analogy.

Since the following G is neither Provable nor Refutable in F it forms a Gödel sentence in F.
∃F ⊇ Q (∃G ∈ L(F) (G ↔ ~(F ⊢ G)))

If the above expression evaluates to False it refutes every Gödel sentence in every F ⊇ Q.

Copyright 2018 Pete Olcott
peteolcott
2018-11-06 02:14:49 UTC
Reply
Permalink
Post by peteolcott
Since the following G is neither Provable nor Refutable in F it forms a Gödel sentence in F.
∃F ⊇ Q (∃G ∈ L(F) (G ↔ ~(F ⊢ G)))
That isn't a G. It is a random formula you've constructed that contains reference to the existence of a G for some F, but doesn't specify any particular G (or F, for that matter).
You STILL don't understand what these symbols mean.
Post by peteolcott
If the above expression evaluates to False
It is trivially true.
You STILL don't understand how formal languages work.
EFQ
∃G (G ↔ ~Provable(G)) -- You have already agreed to this
"there exists a proposition that is materially equivalent to a statement of its own unprovability."

(∃G ∈ L(F) (G ↔ ~(F ⊢ G))) -- Same thing with a little more elaboration
"there exists a proposition G in the language of F that is materially equivalent to a statement of its own unprovability."

∃F ⊇ Q (∃G ∈ L(F) (G ↔ ~(F ⊢ G))) --
"there exists a formal system F superset of Robinson Arithmetic such that"
there exists a proposition G in the language of F that is materially equivalent to a statement of its own unprovability."

Copyright 2018 Pete Olcott
peteolcott
2018-11-06 02:44:39 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
Since the following G is neither Provable nor Refutable in F it forms a Gödel sentence in F.
∃F ⊇ Q (∃G ∈ L(F) (G ↔ ~(F ⊢ G)))
That isn't a G. It is a random formula you've constructed that contains reference to the existence of a G for some F, but doesn't specify any particular G (or F, for that matter).
You STILL don't understand what these symbols mean.
Post by peteolcott
If the above expression evaluates to False
It is trivially true.
You STILL don't understand how formal languages work.
∃F ⊇ Q (∃G ∈ L(F) (G ↔ ~(F ⊢ G))) --
"there exists a formal system F superset of Robinson Arithmetic such that"
there exists a proposition G in the language of F that is materially equivalent to a statement of its own unprovability."
Like I said above, that is trivially true: just take F to be Q with ∃G ∈ L(F) (G ↔ ~(F ⊢ G)) as an axiom.
EFQ
Which is impossible when using the conventional meanings of those symbols in symbolic logic.

If we want to break the rules then we can "prove" that a {cat} really is a type of {dog}.

"In every formal system F there does not exist a proposition G that
is materially equivalent to a statement of its own unprovability."

∀F ∈ Formal_Systems ~∃G ∈ L(F) (G ↔ ~(F ⊢ G)))

∴ The conclusion of Gödel's 1931 Incompleteness Theorem is contradicted, no such G exists in any formal system.

Copyright 2018 Pete Olcott
peteolcott
2018-11-06 03:59:28 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
Post by peteolcott
Since the following G is neither Provable nor Refutable in F it forms a Gödel sentence in F.
∃F ⊇ Q (∃G ∈ L(F) (G ↔ ~(F ⊢ G)))
That isn't a G. It is a random formula you've constructed that contains reference to the existence of a G for some F, but doesn't specify any particular G (or F, for that matter).
You STILL don't understand what these symbols mean.
Post by peteolcott
If the above expression evaluates to False
It is trivially true.
You STILL don't understand how formal languages work.
∃F ⊇ Q (∃G ∈ L(F) (G ↔ ~(F ⊢ G))) --
"there exists a formal system F superset of Robinson Arithmetic such that"
there exists a proposition G in the language of F that is materially equivalent to a statement of its own unprovability."
Like I said above, that is trivially true: just take F to be Q with ∃G ∈ L(F) (G ↔ ~(F ⊢ G)) as an axiom.
Which is impossible when using the conventional meanings of those symbols in symbolic logic.
False.
Post by peteolcott
If we want to break the rules
No rules are broken by adding ∃G ∈ L(F) (G ↔ ~(F ⊢ G)) as an axiom.
Post by peteolcott
∴ The conclusion of Gödel's 1931 Incompleteness Theorem is contradicted, no such G exists in any formal system.
False. It exists in an infinite number of formal systems.
EFQ
Sure and in this same way we can prove that a "cat" is a type of
{dog} by simply assigning the semantic meaning of {poodle} to the
finite string "cat".

This does not work with the conventional semantics associated
with (for example) "⊢".

In this case {cat} and {dog} already have a set of preexisting axioms
such that ~({cat} ◁ {dog}).

◁ is the [is_a_type_of] operator adapted from UML Inheritance relation.

Copyright 2018 Pete Olcott
peteolcott
2018-11-06 02:55:36 UTC
Reply
Permalink
From where have you got the idea that there is such a thing as proof by analogy in mathematics?
What a load of horseshit. Analogies are inherently non-exhaustive. That's what makes them analogies rather than the real thing.
If every sentence that asserts its own unprovability is proven to be
non-existent,
That is impossible, and trivially so. Just consider any formal system in which ∃G (G ↔ ~⊢ G) is an axiom. There are an infinite number of such formal systems, so it's pretty easy to find them. Just take any any formal system you like, then add ∃G (G ↔ ~⊢ G) as an axiom.
EFQ
When we are constrained by the conventional meaning of these symbols in
symbolic logic any "axiom" that contradicts these meanings is rejected
as unsound.

Copyright Pete Olcott
peteolcott
2018-11-06 04:09:46 UTC
Reply
Permalink
From where have you got the idea that there is such a thing as proof by analogy in mathematics?
What a load of horseshit. Analogies are inherently non-exhaustive. That's what makes them analogies rather than the real thing.
You would understand that I am correct when you understand the inheritance relations in knowledge ontologies.
Two things share an identical set of properties inherited from their base class.

A cow and a pig are analogous in the that share all of the properties of mammal.
If we can prove that mammals do not exist then this proves that cows and pigs do not exist.

I proved that the category of {Gödel sentence} is empty:

http://liarparadox.org/index.php/2018/11/04/godels-1931-incompleteness-theorem-as-simple-as-possible/
If every sentence that asserts its own unprovability is proven to be
non-existent,
That is impossible, and trivially so. Just consider any formal system in which ∃G (G ↔ ~⊢ G) is an axiom. There are an infinite number of such formal systems, so it's pretty easy to find them. Just take any any formal system you like, then add ∃G (G ↔ ~⊢ G) as an axiom.
EFQ
peteolcott
2018-11-06 19:29:51 UTC
Reply
Permalink
∀x Bachelor(x) → ~Married(x)
∀x Bachelor(x) ⊢ ~Married(x)
You've ALMOST learned the difference between a formal system and a metalanguage. I say "almost", because I suspect you still think those two expressions belong to the same language.
They are defined to be in the same language.
Oh dear. Then you lied when you said you were using the "conventional meaning" of these symbols.
Before you can progress any further, you need to define the syntactic, deductive, and semantic rules relevant to ⊢, because it is not "conventionally" taken to be part of a formal system itself. It "conventionally" exists in the metalanguage only, as a way to talk about the deductive rules of a formal system.
Syntactic: if P is a WFF, then ~P is a WFF
Syntactic: if P and Q are WFFs, then (P & Q) is a WFF
Deductive: ~~P ⊢P
Deductive: (P & Q) ⊢P
Semantic: V(~P)=1 iff V(P)=0
Semantic: V(P & Q)=1 iff V(P)=1 and V(Q)=1
Again, note that these are rules in the metalanguage, talking about properties of the formal system. Are you SURE you want ⊢ down in the formal system itself, rather than up in the metalanguage where it "conventionally" belongs?
EFQ
Your V(P)=1 is only really saying that True(P) is satisfied, likewise
for V(Q)=0 only meaning that False(Q) is satisfied.

I do not see any need for a metalanguage M to specify the semantics
of any formal language L when this semantics can be expressed directly
in the syntax of L.

There is definitely a need for a formal metalanguage M to express the
formal semantics of natural language N.

The conventional symbols of symbolic logic (including ⊢) do have
conventional semantics specified in English: (See Mendelson).

To make it clear enough that a machine can understand them requires
formalizing the conventional English semantics of these logical
operators.

It seems to me that this semantics could be formalized by simply
defining their syntactic relation to other symbols.

We don't really need to be clear enough for a machine to understand:

"In every formal system F there does not exist a proposition G that --
is materially equivalent to a statement of its own unprovability." --
∀F ∈ Formal_Systems ~∃G ∈ L(F) (G ↔ ~(F ⊢ G))) --
∴ ~∃ Gödel_Sentence(G) in any form besides misconception. --

Copyright 2018 Pete Olcott
peteolcott
2018-11-07 05:29:23 UTC
Reply
Permalink
Post by peteolcott
∀x Bachelor(x) → ~Married(x)
∀x Bachelor(x) ⊢ ~Married(x)
You've ALMOST learned the difference between a formal system and a metalanguage. I say "almost", because I suspect you still think those two expressions belong to the same language.
They are defined to be in the same language.
Oh dear. Then you lied when you said you were using the "conventional meaning" of these symbols.
Before you can progress any further, you need to define the syntactic, deductive, and semantic rules relevant to ⊢, because it is not "conventionally" taken to be part of a formal system itself. It "conventionally" exists in the metalanguage only, as a way to talk about the deductive rules of a formal system.
Syntactic: if P is a WFF, then ~P is a WFF
Syntactic: if P and Q are WFFs, then (P & Q) is a WFF
Deductive: ~~P ⊢P
Deductive: (P & Q) ⊢P
Semantic: V(~P)=1 iff V(P)=0
Semantic: V(P & Q)=1 iff V(P)=1 and V(Q)=1
Again, note that these are rules in the metalanguage, talking about properties of the formal system. Are you SURE you want ⊢ down in the formal system itself, rather than up in the metalanguage where it "conventionally" belongs?
Your V(P)=1 is
.... conventional notation.
If you want to use something else, you have to define it.
Post by peteolcott
I do not see any need for a metalanguage M
Because you're an idiot, apparently.
Post by peteolcott
to specify the semantics
of any formal language L when this semantics can be expressed directly
in the syntax of L.
That makes no sense. "True()" doesn't mean true because it's called "True()". There is no difference in meaning between calling a logical predicate "True()" and calling it "Fuzzy()".
The semantics tells you what any bit of logic means. The English language letters you use to label your predicate do not tell you the meaning.
EFQ
And if insert the concept of metalanguage V(P)=1 directly into the
object language you can do this simply as ⊢P

Copyright 2018 Pete Olcott
peteolcott
2018-11-07 07:16:33 UTC
Reply
Permalink
Post by peteolcott
The semantics tells you what any bit of logic means. The English language letters you use to label your predicate do not tell you the meaning.
And if insert the concept of metalanguage V(P)=1 directly into the
object language you can do this simply as ⊢P
Good grief, you get dumber with every post.
V(P)=1 means M ⊨ P. It does NOT mean ⊢ P.
Just because something is true in a model does not mean it is a theorem!
EFQ
Yes a learned by rote logician knowing conventional wisdom would say that.

A philosophy of logic person that reverse-engineers the underpinnings of the
foundations of logic might examine the possibilities and propose that the
Tarski object language metalanguage distinction might be made unnecessary
if what-so-ever can be expressed in the metalanguage is made expressible
directly in the object language.

If V(P)=1 in the metalanguage is construed to possibly be represented in the
object language as ⊢P, and this hypothesis is actually tested instead of
being rejected out-of-hand simply because it is unconventional new insights
might be attained.

Of course this must further assume the other unconventional idea that ⊢
is also directly represented in the object language. If this is an
analytical impossibility (such as square circles) please show it.
If it is simply unconventional then I propose that your mind is closed
to possibilities.

Copyright 2018 Pete Olcott
peteolcott
2018-11-07 18:36:52 UTC
Reply
Permalink
Post by peteolcott
The semantics tells you what any bit of logic means. The English language letters you use to label your predicate do not tell you the meaning.
And if insert the concept of metalanguage V(P)=1 directly into the
object language you can do this simply as ⊢P
Good grief, you get dumber with every post.
V(P)=1 means M ⊨ P. It does NOT mean ⊢ P.
Just because something is true in a model does not mean it is a theorem!
Yes
Indeed. These are the "conventional meanings" of these symbols, which are the meanings you claimed to be using. If you are in fact using different meanings, then you are a liar. Furthermore, you shouldn't assign different meanings to existing notation; use different notation, and give rigorous definitions for it.
The real problem, of course, is that you claim to be using "conventional meaning", but you don't even know what that is. So you're both an idiot and a liar.
EFQ
Orrrrr, I could be using the conventional meaning of these symbols in an unconventional context.

I am using the symbols with their exact conventional semantics directly in the object language and not in the metalanguage.

Same symbols, same meaning, different context.

If you try to prove that this is logically incoherent instead of merely unconventional you might be able to understand.

You have so far only been saying: "You are wrong, you are wrong, because we just don't do it that way".

Copyright 2018 Pete Olcott
peteolcott
2018-11-07 18:43:35 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
The semantics tells you what any bit of logic means. The English language letters you use to label your predicate do not tell you the meaning.
And if insert the concept of metalanguage V(P)=1 directly into the
object language you can do this simply as ⊢P
Good grief, you get dumber with every post.
V(P)=1 means M ⊨ P. It does NOT mean ⊢ P.
Just because something is true in a model does not mean it is a theorem!
Yes
Indeed. These are the "conventional meanings" of these symbols, which are the meanings you claimed to be using. If you are in fact using different meanings, then you are a liar. Furthermore, you shouldn't assign different meanings to existing notation;
use different notation, and give rigorous definitions for it.
The real problem, of course, is that you claim to be using "conventional meaning", but you don't even know what that is. So you're both an idiot and a liar.
EFQ
Orrrrr, I could be using the conventional meaning of these symbols in an unconventional context.
I am using the symbols with their exact conventional semantics directly in the object language and not in the metalanguage.
Same symbols, same meaning, different context.
If you try to prove that this is logically incoherent instead of merely unconventional you might be able to understand.
You have so far only been saying: "You are wrong, you are wrong, because we just don't do it that way".
Copyright 2018 Pete Olcott
Bureaucrats have this same sort of reasoning never realizing that it is circular thus fallacious:

"You are wrong, you are wrong, because we just don't do it that way".
Why not?
"Because its just not done!"

If you cannot find logical incoherence in my specification then any rebuttal is worth zilch.
peteolcott
2018-11-08 05:31:08 UTC
Reply
Permalink
See my new thread.
No, crank. I'm not going to play whack-a-mole. Respond to me directly. I'm not going to chase down each and every one of the tiniest iterations of your rantings. Keep it in one thread.
EFQ
I forgot that my title already included Tarski. I will keep the
same title and only change version numbers. That way it is clear
that we are on a newer version of the exactly same general subject.

Does anyone here have more than a dogmatic belief in the following?
Can anyone provide the details of the reasoning proving that it
is necessary?

The best way for me to prove that it is not necessary is to provide
a correct rebuttal to any proof that it is necessary. I can do that
with reasoning, I cannot do that with dogma.

Page 273
A. For every formalized language a formally correct and materially
adequate definition of true sentence can be constructed in the
metalanguage with the help only of general logical expressions, of
expressions of the language itself, and of terms from the morphology
of language – but under the condition that the metalanguage possesses
a higher order than the language which is the object of investigation.
B. If the order of the metalanguage is at most equal to that of the
language itself, such a definition cannot be constructed.
peteolcott
2018-11-08 06:14:38 UTC
Reply
Permalink
Post by peteolcott
See my new thread.
No, crank. I'm not going to play whack-a-mole. Respond to me directly. I'm not going to chase down each and every one of the tiniest iterations of your rantings. Keep it in one thread.
I forgot that my title already included Tarski. I will keep the
same title and only change version numbers.
No. Keep it in one thread, with the same title, in a normal discussion like a sane person. Your "versions" don't warrant new thread numbering, since every time you update your idiocy, you just introduce yet another mistake. Usenet is not your personal notepad.
EFQ
So I guess that as hominem is all that you got now you cannot
refute my reply because it is irrefutable and you know it.

I was wondering what you would do when I finally proved my point.
Your total lack of anything resembling a rebuttal for quite a few
recent replies seems to answer that question.

I guess that you are stuck in rebuttal mode and shooting the blanks
of ad hominem proves that you are out of ammo in terms of correct
reasoning to show any errors on my part.

You did a very excellent job in helping me strip away unclarity.

Direct quote from page 275
We can construct a sentence x which satisfies the following condition:
It is not true that x ∈ Pr if and only if p
...
(1) x ∉ Pr ↔ p
Where the symbol 'p' represents the whole sentence x.

In other words:
p ∉ Pr ↔ p

In other words:
p ∉ Provable ↔ p

In other words:
p ↔ ~Provable(p)

Copyright 2018 Pete Olcott
peteolcott
2018-11-08 07:18:44 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
See my new thread.
No, crank. I'm not going to play whack-a-mole. Respond to me directly.. I'm not going to chase down each and every one of the tiniest iterations of your rantings. Keep it in one thread.
I forgot that my title already included Tarski. I will keep the
same title and only change version numbers.
No. Keep it in one thread, with the same title, in a normal discussion like a sane person. Your "versions" don't warrant new thread numbering, since every time you update your idiocy, you just introduce yet another mistake. Usenet is not your personal notepad.
So I guess that as hominem is all that you got
It's all you deserve.
I have tried to play nice. I have given you countless hours of my expertise and advice, and it got the discussion nowhere. You repaid every instance of my intellectual generosity with endless repetition of your stubborn refusal to learn, and to this day, in the most recent cutting edge "update" to your imbecilic ranting, you STILL make the same pathetic elementary mistakes you've been making since your first post.
You are clearly not interested in understanding.
You are clearly not interested in facts.
You are just a self-centred moron, too much of an idiot to understand why you are wrong, and too arrogant and lazy to try to correct your ignorance.
You splatter your ranting all over the newsgroup, in thread after thread, with the tiniest of changes here and there, none of which brings you closer to being correct.
Post by peteolcott
Direct quote from page 275
[snip]
Just like the various definitions and out-of-context quotes you are fond on endlessly repeating, you are once again posting something you clearly don't understand.
It contradicts you, dumbass.
You are such a monumental idiot >
And you know, that would be fine, if you had any motivation at all to improve yourself. But you're a lazy asshole, too, so you're just going to remain a monumental idiot.
EFQ
YOU CAN NOT SHOW ANY ERROR IN THE ESSENCE OF THE REASONING PROVIDED BELOW

Tarski quote page 275
We can construct a sentence x which satisfies the following condition:
It is not true that x ∈ Pr if and only if p
(1) x ∉ Pr ↔ p // p ↔ ~Provable(p)

When Tarski's expression above is transformed into this:
p ↔ ~Provable(p)

It is easily rebutted when its refutation is boiled down to its
barest possible essence:

∃G (G ↔ ~Provable(G))
“there exists a proposition that is materially equivalent to a statement of its own unprovability.” EFQ quote

If G was Provable this contradicts its assertion: G is not Provable.
If ~G was Provable this contradicts its assertion: G is Provable
Therefore G is neither Provable nor Refutable and does not exist.

Copyright 2018 Pete Olcott

http://liarparadox.org/index.php/2018/11/04/godels-1931-incompleteness-theorem-as-simple-as-possible/
peteolcott
2018-11-08 17:00:20 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
Post by peteolcott
See my new thread.
No, crank. I'm not going to play whack-a-mole. Respond to me directly.. I'm not going to chase down each and every one of the tiniest iterations of your rantings. Keep it in one thread.
I forgot that my title already included Tarski. I will keep the
same title and only change version numbers.
No. Keep it in one thread, with the same title, in a normal discussion like a sane person. Your "versions" don't warrant new thread numbering, since every time you update your idiocy, you just introduce yet another mistake. Usenet is not your personal notepad.
So I guess that as hominem is all that you got
It's all you deserve.
I have tried to play nice. I have given you countless hours of my expertise and advice, and it got the discussion nowhere. You repaid every instance of my intellectual generosity with endless repetition of your stubborn refusal to learn, and to this day, in the most recent cutting edge "update" to your imbecilic ranting, you STILL make the same pathetic elementary mistakes you've been making since your first post.
You are clearly not interested in understanding.
You are clearly not interested in facts.
You are just a self-centred moron, too much of an idiot to understand why you are wrong, and too arrogant and lazy to try to correct your ignorance.
You splatter your ranting all over the newsgroup, in thread after thread, with the tiniest of changes here and there, none of which brings you closer to being correct.
Post by peteolcott
Direct quote from page 275
[snip]
Just like the various definitions and out-of-context quotes you are fond on endlessly repeating, you are once again posting something you clearly don't understand.
It contradicts you, dumbass.
You are such a monumental idiot >
And you know, that would be fine, if you had any motivation at all to improve yourself. But you're a lazy asshole, too, so you're just going to remain a monumental idiot.
YOU CAN NOT SHOW ANY ERROR IN THE ESSENCE OF THE REASONING PROVIDED BELOW
Therefore G
[snip]
Post by peteolcott
and does not exist.
False.
Again, you remain a monumental idiot.
Where did you get the stupid idea that being undecidable was impossible?
Being undecidable is not impossible
I know it's not, you monumental idiot. That's why I asked you why YOU are trying to derive a conclusion that in context suggests that being undecidable is impossible.
If G was Provable this contradicts its assertion: G is not Provable.
If ~G was Provable this contradicts its assertion: G is Provable
Therefore G is neither Provable nor Refutable and does not exist.
Make up your mind, monumental idiot.
EFQ
You are not a monumental idiot, you are at least near genius.
A near genius that gets a little frustrated remains a near genius.

The average person speaking to me here has the intelligence and knowledge of an MS in math.
The range of this knowledge and ability would be between bachelors degree and PhD.

All in all I have gotten the highest quality reviews in this forum that are greater
than every other forum besides comp.theory in its heyday, then sci.logic = comp.theory.
It might be the case that you are my best overall reviewer ever.

X ↔ (∃p (p ↔ ~Provable(p)))
Does X evaluate to True, False or Neither?

http://liarparadox.org/index.php/2018/11/08/refuting-tarski-1936-undefinability-theorem/

Copyright Pete Olcott
peteolcott
2018-11-08 18:11:58 UTC
Reply
Permalink
Post by peteolcott
X ↔ (∃p (p ↔ ~Provable(p)))
Does X evaluate to True, False or Neither?
How many times are you going to post this?
Post it once (or never), and then STOP.
Did your brain cell twitch when you hit send?
How can we know how to "evaluate" X if you don't define which formal system you're talking about (let alone the model being used for interpretation)?
Just like I have already been saying to you long before I read this paragraph from
Tarski for the very first time last night:

Page 276
...the metatheory can be interpreted IN THE THEORY [itself] enriched by variables
of higher order and since in this interpretation the sentence x, which contains
no specific term of the metatheory, is its own correlate, the proof of the sentence
x given in the metatheory can be automatically carried over to the theory itself...

MTT is merely FOPL with variables from 0 to N order of logic and the key augmentation
of a Provability logical operator, thus the exact same thing that Tarski is referring to.

https://www.researchgate.net/publication/317953772_Provability_with_Minimal_Type_Theory

The above YACC BNF was left intentionally incomplete in that the key syntax required
for defining the lower order logic of HOL variables is only explained and not explicitly
encoded in this YACC BNF. More recent unpublished versions have this syntax encoded.

Copyright 2018 Pete Olcott
peteolcott
2018-11-08 19:34:30 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
X ↔ (∃p (p ↔ ~Provable(p)))
Does X evaluate to True, False or Neither?
How many times are you going to post this?
Post it once (or never), and then STOP.
Did your brain cell twitch when you hit send?
How can we know how to "evaluate" X if you don't define which formal system you're talking about (let alone the model being used for interpretation)?
MTT is
It's horseshit, is what it is. You have never offered a full formal specification, so it's worthless.
How is the YACC BNF on the first page of this not an almost totally complete formal specification of WFF(MTT) ?
https://www.researchgate.net/publication/317953772_Provability_with_Minimal_Type_Theory
peteolcott
2018-11-10 00:39:18 UTC
Reply
Permalink
    This sentence is false.
Which Tarski examined as: This sentence cannot be proven."
No, he most certainly did not. Tarksi would not make such an elementary mistake as confusing truth with provability. Anyone with even normal intelligence who studied logic for any reasonable amount of time would know the difference.
http://liarparadox.org/index.php/2018/11/09/simplifying-the-tarski-undefinability-sentence/

Tarski 1936 Page 275
Undefinability Theorem sentence basis of the Undefinability Theorem:
We can construct a sentence x … which satisfies the following condition:
It is not true that x ∈ Pr if and only if p

(1) x ∉ Pr ↔ p
Where the symbol ‘p’ represents the whole sentence x.

We shall show that the sentence x is actually undecidable and at the same
time true.

<light hearted sarcasm>
OK then, if we expand "Pr" he must have been talking about Pringles potato chips
when specifying his Undefinability Theorem sentence rather than:
"the class of all provable sentences of the theory under consideration"

And his Undefinability Theorem pertained to the Undefinability of potato chips
rather than the Undefinability of the formal notion of Truth.
</light hearted sarcasm>

Alternatively his Theorem regarding the Undefinability of
x ∈ the class of all true sentences: True(x)

is based on his Undefinability sentence that is specified using
x ∈ the class of all provable sentences: Provable(x)

Copyright 2018 Pete Olcott
peteolcott
2018-11-10 02:10:40 UTC
Reply
Permalink
Post by peteolcott
    This sentence is false.
Which Tarski examined as: This sentence cannot be proven."
No, he most certainly did not. Tarksi would not make such an elementary mistake as confusing truth with provability. Anyone with even normal intelligence who studied logic for any reasonable amount of time would know the difference.
Tarski 1936 Page 275
We shall show that the sentence x is actually undecidable and at the same
time true.
See? Your quote proved me right!
Why don't you bother to read what you post before you post it?
EFQ
The Tarski Undefinability Theorem was about the Undefinability
of True(x) defined as x ∈ the class of all true sentences.

The Tarski Undefinability sentence was about Provable(x)
defined as: x ∈ the class of all provable sentences.

Tarski 1936 Page 275
the symbol 'Pr' which denotes the class of all provable sentences
Undefinability Theorem sentence basis of the Undefinability Theorem:
We can construct a sentence x … which satisfies the following condition:
It is not true that x ∈ Pr if and only if p
...
(1) x ∉ Pr ↔ p
...
we denote the class of all true sentences by the symbol "Tr"

He did not confuse Truth with Provability he proved Undefinability of True(x)
based on Incompleteness of Provable(x), just like I said.
Peter T. Daniels
2018-11-08 21:18:14 UTC
Reply
Permalink
Post by peteolcott
All in all I have gotten the highest quality reviews in this forum that are greater
than every other forum besides comp.theory in its heyday, then sci.logic = comp.theory.
I trust "this forum" is not sci.lang. Please stop crossposting here.
peteolcott
2018-11-09 04:48:46 UTC
Reply
Permalink
Post by Peter T. Daniels
Post by peteolcott
All in all I have gotten the highest quality reviews in this forum that are greater
than every other forum besides comp.theory in its heyday, then sci.logic = comp.theory.
I trust "this forum" is not sci.lang. Please stop crossposting here.
I have never gotten any linguistic reviews of anything that I have ever
said in any forum besides this one: sci.lang.
Peter T. Daniels
2018-11-09 13:36:49 UTC
Reply
Permalink
Post by peteolcott
Post by Peter T. Daniels
Post by peteolcott
All in all I have gotten the highest quality reviews in this forum that are greater
than every other forum besides comp.theory in its heyday, then sci.logic = comp.theory.
I trust "this forum" is not sci.lang. Please stop crossposting here.
I have never gotten any linguistic reviews of anything that I have ever
said in any forum besides this one: sci.lang.
Who in this forum, sci.lang, has done such a thing?
peteolcott
2018-11-09 16:00:09 UTC
Reply
Permalink
Post by Peter T. Daniels
Post by peteolcott
Post by Peter T. Daniels
Post by peteolcott
All in all I have gotten the highest quality reviews in this forum that are greater
than every other forum besides comp.theory in its heyday, then sci.logic = comp.theory.
I trust "this forum" is not sci.lang. Please stop crossposting here.
I have never gotten any linguistic reviews of anything that I have ever
said in any forum besides this one: sci.lang.
Who in this forum, sci.lang, has done such a thing?
You for one.
Peter T. Daniels
2018-11-09 21:43:30 UTC
Reply
Permalink
Post by peteolcott
Post by Peter T. Daniels
Post by peteolcott
Post by Peter T. Daniels
Post by peteolcott
All in all I have gotten the highest quality reviews in this forum that are greater
than every other forum besides comp.theory in its heyday, then sci.logic = comp.theory.
I trust "this forum" is not sci.lang. Please stop crossposting here.
I have never gotten any linguistic reviews of anything that I have ever
said in any forum besides this one: sci.lang.
Who in this forum, sci.lang, has done such a thing?
You for one.
? When have I ever said anything about the content of any of your messages,
other than to point out that you're not doing linguistics?
peteolcott
2018-11-09 17:19:53 UTC
Reply
Permalink
expressions of the next increment of logical order from named expressions
of the next lower order using slightly augmented FOPL syntax.
How? You're still just handwaving without giving any rigorous definitions.
Maybe if it was a new logical operator I would need those things.

LHS @ RHS The <alias name> “@” operator specifies macro substitution:
Every occurrence of the LHS {alias name} encountered in any RHS {body}
is replaced with the the RHS {body} referenced by the LHS {alias name}
by the semantic interpreter.

LiarParadox @ ~True(LiarParadox)
LiarParadox @ ~⊢LiarParadox

The following syntax may not quite perfectly express the semantics that I intend.
The first expression is intended to specify a set of languages:
The language of every formal system that is a superset of Robinson Arithmetic.
Q @ ∀(F ∈ Formal_Systems ∧ F ⊇ Robinson_Arithmetic) Language(F)

∃G ∈ Q (G ↔ ~(F ⊢ G))
Besides the "⊢" that may still be all logic of the first order.
It seems to me that "⊢" would inherit its logic order on a case-by-case
basis from its argument.

Arithmetic ⊢ "2 + 3 = 5"
Would simple have the logic order Arithmetic Axioms. We might generalize
this to say that ⊢ always has the logic order of the axioms of the formal system.

Copyright 2018 Pete Olcott
one or more syntactic rules defining WFFs in F with your new operator as a main connective, one or more deductive rules showing how WFFs containing this new operator contribute to proofs in F, and one or more semantic rules showing how WFFs containing this new operator as a main connective are interpreted in a model M.
syntactic: if P and Q are WFFs, then P&Q and Q&P are both WFFs
deductive: if P and Q are entries in a proof, then P&Q and Q&P can be later entries in the same proof
deductive: if P&Q is an entry in a proof, then P and Q can be later entries in the same proof
semantic: V(P&Q)=1 iff V(P)=1 and V(Q)=1; that is, P&Q is true in a model iff both P and Q are true in the same model)
EFQ
peteolcott
2018-11-09 22:43:04 UTC
Reply
Permalink
Post by peteolcott
expressions of the next increment of logical order from named expressions
of the next lower order using slightly augmented FOPL syntax.
How? You're still just handwaving without giving any rigorous definitions.
Maybe if it was a new logical operator I would need those things.
It is new to first-order predicate logic.
There is no such thing as "macro substitution" in first-order predicate logic.
Post by peteolcott
Every occurrence of the LHS {alias name} encountered in any RHS {body}
syntactic: if P and Q are WFFs, then P&Q and Q&P are both WFFs
deductive: if P and Q are entries in a proof, then P&Q and Q&P can be later entries in the same proof
deductive: if P&Q is an entry in a proof, then P and Q can be later entries in the same proof
semantic: V(P&Q)=1 iff V(P)=1 and V(Q)=1; that is, P&Q is true in a model iff both P and Q are true in the same model)
Post by peteolcott
is replaced
"Replaced" *HOW*? What does it actually mean to "replace" something in your system? Are you just talking about extensional meaning? If so, why not say so? It's hardly a new concept, and many people have talked about it much more rigorously than you seem capable of. If it's not what you mean, how is is what you're doing different from that?
Post by peteolcott
The following syntax may not quite perfectly express the semantics that I intend.
SYNTAX DOESN'T EXPRESS SEMANTICS, DUMBASS. HOW MANY FUCKING TIMES DO YOU NEED TO BE TOLD THIS?
EFQ
https://en.wikipedia.org/wiki/Second-order_logic
second-order logic, in addition, also quantifies over relations. For example,
the second-order sentence ∀P∀x(x ∈ P ∨ x ∉ P) says that for every unary
relation (or set) P of individuals, and every individual x, either x is in
P or it is not (this is the principle of bivalence).

Second order logic expressed as two linked levels of FOL using MTT syntax
Bivalence(x, P) @ ( ∈(x,P) ∨ ~∈(x,P) )
∀P∀x Bivalence(x, P)

This is the first time that I ever tried this so it may be wrong.

This would seem to do the same thing:
∀P∀x ( ∈(x,P) ∨ ~∈(x,P) )

Copyright 2018 Pete Olcott
peteolcott
2018-11-10 04:32:33 UTC
Reply
Permalink
Post by peteolcott
expressions of the next increment of logical order from named expressions
of the next lower order using slightly augmented FOPL syntax.
How? You're still just handwaving without giving any rigorous definitions.
Maybe if it was a new logical operator I would need those things.
It is new to first-order predicate logic.
There is no such thing as "macro substitution" in first-order predicate logic.
Post by peteolcott
Every occurrence of the LHS {alias name} encountered in any RHS {body}
syntactic: if P and Q are WFFs, then P&Q and Q&P are both WFFs
deductive: if P and Q are entries in a proof, then P&Q and Q&P can be later entries in the same proof
deductive: if P&Q is an entry in a proof, then P and Q can be later entries in the same proof
semantic: V(P&Q)=1 iff V(P)=1 and V(Q)=1; that is, P&Q is true in a model iff both P and Q are true in the same model)
Post by peteolcott
is replaced
"Replaced" *HOW*? What does it actually mean to "replace" something in your system? Are you just talking about extensional meaning? If so, why not say so? It's hardly a new concept, and many people have talked about it much more rigorously than you seem capable of. If it's not what you mean, how is is what you're doing different from that?
Post by peteolcott
The following syntax may not quite perfectly express the semantics that I intend.
SYNTAX DOESN'T EXPRESS SEMANTICS, DUMBASS. HOW MANY FUCKING TIMES DO YOU NEED TO BE TOLD THIS?
[snip]
None of this addresses what I said.
I (possibly incorrectly, no feedback yet) interpreted Percival's advice to
mean that this might be syntactically correct:

Q ↔df ∀(F ∈ Formal_Systems ∧ F ⊇ Robinson_Arithmetic)
L ↔df Language(Q)
∃G ∈ L (G ↔ ~(F ⊢ G))

Copyright 2018 Pete Olcott
If so, write <->df between formulae and =df between terms.
then you still need to say what it is, i.e., what its syntax and semantics are.
Peter Percival
2018-11-10 04:57:14 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
expressions of the next increment of logical order from named expressions
of the next lower order using slightly augmented FOPL syntax.
How? You're still just handwaving without giving any rigorous definitions.
You need at least three things to add a new logical operator to
Maybe if it was a new logical operator I would need those things.
It is new to first-order predicate logic.
There is no such thing as "macro substitution" in first-order predicate logic.
Post by peteolcott
Every occurrence of the LHS {alias name} encountered in any RHS {body}
"Any occurrence" *WHERE*? In formulas of the formal system? In
deductive proofs in the formal system? In statements about the
assignment or an extensional assignment? What PRECISELY can appear
it a WFF of your formal system or a statement in the metalanguage?
Your informal shitty handwaving nonsense is useless. Without a
careful, rigorous, formal definition, nothing you say can be
properly evaluated. For example, some of the relevant careful,
syntactic: if P and Q are WFFs, then P&Q and Q&P are both WFFs
deductive: if P and Q are entries in a proof, then P&Q and Q&P can
be later entries in the same proof
deductive: if P&Q is an entry in a proof, then P and Q can be
later entries in the same proof
semantic: V(P&Q)=1 iff V(P)=1 and V(Q)=1; that is, P&Q is true in
a model iff both P and Q are true in the same model)
Post by peteolcott
is replaced
"Replaced" *HOW*? What does it actually mean to "replace"
something in your system? Are you just talking about extensional
meaning? If so, why not say so? It's hardly a new concept, and
many people have talked about it much more rigorously than you
seem capable of. If it's not what you mean, how is is what you're
doing different from that?
Post by peteolcott
The following syntax may not quite perfectly express the
semantics that I intend.
SYNTAX DOESN'T EXPRESS SEMANTICS, DUMBASS. HOW MANY FUCKING TIMES
DO YOU NEED TO BE TOLD THIS?
[snip]
None of this addresses what I said.
I (possibly incorrectly, no feedback yet) interpreted Percival's advice to
Q ↔df ∀(F ∈ Formal_Systems ∧ F ⊇ Robinson_Arithmetic)
How do you read "∀(F ∈ Formal_Systems ∧ F ⊇ Robinson_Arithmetic)"? Tell
me in plain English.
Post by peteolcott
L ↔df Language(Q)
∃G ∈ L (G ↔ ~(F ⊢ G))
Learn what is meant by the language of a theory. Then ask yourself if G
is meant to be a formula, and if "∃G ∈ L" makes sense.
Post by peteolcott
Copyright 2018 Pete Olcott
If so, write <->df between formulae and =df between terms.
then you still need to say what it is, i.e., what its syntax and
semantics are.
--
"He who will not reason is a bigot;
he who cannot is a fool;
he who dares not is a slave."
- Sir William Drummond
peteolcott
2018-11-10 04:41:25 UTC
Reply
Permalink
When I say True(x), I am referring to Tarksi: "the class of all true sentences"
except there is no need to: "pass it to a metatheory of a higher order".
THEN YOU AREN'T REFERRING TO WHAT TARSKI MEANS, SO STOP SAYING YOU ARE!
I mean exactly what he means except that I eliminated one whole level of
extraneous complexity.

The proof that my simplification is correct is that my simplification
rejects all of the expressions of language that previously were understood
to show Undefinability or Incompleteness and it ONLY rejects these
expressions of language.

The only way that you are going to possibly understand what I am saying
is for you to try and provide reasoning that contradicts the exact
claim that I just made.

If you know that you cannot possibly do that because you know that
I already unequivocally proved this point, then continue with your:
"That's just not the way that we do thing here" arguments (to no avail).
peteolcott
2018-11-10 05:02:06 UTC
Reply
Permalink
Q ↔ ∀F (Formal_Systems(F) ∧ Superset(Robinson_Arithmetic, F))
L ↔ Language(Q)
∃G ∈ L (G ↔ ~(F ⊢ G))
SQ ↔df ∀(F ∈ Formal_Systems ∧ F ⊇ Robinson_Arithmetic)
L ↔df Language(SQ)
∃G ∈ L (G ↔ ~(F ⊢ G))

So is the above syntactically correct?

"This sentence is not provable"
Does this formalization precisely correspond to the English?
G ↔df ~Provable(G)

These are some of the other symbols suggested:
https://math.stackexchange.com/questions/944757/whats-the-most-right-symbol-to-use-for-defined-to-be-equal-to
peteolcott
2018-11-10 05:17:08 UTC
Reply
Permalink
Post by peteolcott
Q ↔ ∀F (Formal_Systems(F) ∧ Superset(Robinson_Arithmetic, F))
L ↔ Language(Q)
∃G ∈ L (G ↔ ~(F ⊢ G))
SQ ↔df ∀(F ∈ Formal_Systems ∧ F ⊇ Robinson_Arithmetic)
L  ↔df  Language(SQ)
∃G ∈ L (G ↔ ~(F ⊢ G))
So is the above syntactically correct?
"This sentence is not provable"
Does this formalization precisely correspond to the English?
G ↔df ~Provable(G)
https://math.stackexchange.com/questions/944757/whats-the-most-right-symbol-to-use-for-defined-to-be-equal-to
https://en.wikipedia.org/wiki/List_of_logic_symbols
x := y means x is defined to be another name for y
There already was an <assign alias name> operator

So it looks like your idea was very helpful proving that your knowledge may
extend into at least MS(math). It seems that your suggestion was an element
of a whole class of <assign alias name> operators, only Wikipedia called it that.
peteolcott
2018-11-08 17:03:30 UTC
Reply
Permalink
Post by peteolcott
Yes a learned by rote logician knowing conventional
wisdom would say that.
If you said that dogs do not give birth to kittens,
and I answered you that, if we define cats as dogs,
then dogs do give birth to kittens, how would you
respond?
Would you accept my argument that dogs can give birth
to kittens?
That would be rejected on the basis of contradicting
preexisting axioms.
These axioms of which you speak are intended to describe
how English is used. In the usual way that English is used,
what we call dogs do not give birth to what we call kittens.
I'm not objecting to that, that normal sort of understanding
of the language (whatever particular problems there may be
with some particular understanding).
I am pointing out that, if you were consistent in how you
did your rejecting-on-the-basis-of-preexisting-axioms,
you would reject your own argument-by-redefinition.
All *you* (PO) are doing is defining cats as a kind of dog,
in order to astound and amaze us with your "proof" that
dogs can give birth to kittens. I'm glad that you agree that
the dog/kitten argument should be rejected. But your
argument (all of your arguments, it looks to me) makes the
same kind of error. And yet you don't reject it (or them).
Try reading the pages 275-276 of Tarski's Undefinability
http://www.thatmarcusfamily.org/philosophy/Course_Websites/Readings/Tarski%20-%20The%20Concept%20of%20Truth%20in%20Formalized%20Languages.pdf
All I can say to that is, "Yes, okay, and then what?"
The following five lines are a direct quote from page 275 of Tarski:
We can construct a sentence x which satisfies the following condition:
It is not true that x ∈ Pr if and only if p

(1) x ∉ Pr ↔ p
Where the symbol ‘p’ represents the whole sentence x.

In other words:
p ∉ Pr ↔ p

In other words:
p ∉ Provable ↔ p

In other words:
p ↔ ~Provable(p)

add an existential quantifier
∃p (p ↔ ~Provable(p))

[sci.logic exflaso.quodlibet quoted paraphrase of the above expression]
“there exists a proposition that is materially equivalent to a statement of its own unprovability.”

If p was Provable this contradicts its assertion: p is not Provable.
If ~p was Provable this contradicts its assertion: p is Provable.
Thus p is a Gödel sentence.

X ↔ (∃p (p ↔ ~Provable(p)))
Does X evaluate to True, False or Neither?

Copyright 2018 Pete Olcott

http://liarparadox.org/index.php/2018/11/08/refuting-tarski-1936-undefinability-theorem/
Peter Percival
2018-11-09 11:25:43 UTC
Reply
Permalink
sci.lang removed
Post by peteolcott
It is not true that x ∈ Pr if and only if p

(1) x ∉ Pr ↔ p
Where the symbol ‘p’ represents the whole sentence x.
p ∉ Pr ↔ p
What sanctions the substitution of 'p' for 'x'? Are they of the same
type? As the genius inventor of a theory of types, you will have
addressed such matters. What's the answer in this particular case?
Post by peteolcott
p ∉ Provable ↔ p
p ↔ ~Provable(p)
add an existential quantifier
∃p (p ↔ ~Provable(p))
[sci.logic exflaso.quodlibet quoted paraphrase of the above expression]
“there exists a proposition that is materially equivalent to a statement
of its own unprovability.”
If p was Provable this contradicts its assertion: p is not Provable.
If ~p was Provable this contradicts its assertion: p is Provable.
Thus p is a Gödel sentence.
X ↔ (∃p (p ↔ ~Provable(p)))
Does X evaluate to True, False or Neither?
Copyright 2018 Pete Olcott
http://liarparadox.org/index.php/2018/11/08/refuting-tarski-1936-undefinability-theorem/
--
"He who will not reason is a bigot;
he who cannot is a fool;
he who dares not is a slave."
- Sir William Drummond
Peter T. Daniels
2018-11-09 13:38:10 UTC
Reply
Permalink
Post by Peter Percival
sci.lang removed
Then why am I seeing this message? (It wasn't quoted by PO.)
peteolcott
2018-11-09 17:34:10 UTC
Reply
Permalink
Post by Peter Percival
sci.lang removed
Post by peteolcott
It is not true that x ∈ Pr if and only if p

(1) x ∉ Pr ↔ p
Where the symbol ‘p’ represents the whole sentence x.
p ∉ Pr ↔ p
What sanctions the substitution of 'p' for 'x'?  Are they of the same type?  As the genius inventor of a theory of types, you will have addressed such matters.  What's the answer in this particular case?
"the symbol ‘p’ represents the whole sentence x."

Tarski's biggest error that he seemed to be stuck on throughout
his career is that the level of indirect reference between an
expression and its name may exist syntactically yet does not
actually exist semantically.

LHS @ RHS The <alias name> “@” operator specifies macro substitution:
Every occurrence of the LHS {alias name} encountered in any RHS {body}
is replaced with the the RHS {body} referenced by the LHS {alias name}
by the semantic interpreter.

LiarParadox @ ~True(LiarParadox)

Copyright 2018 Pete Olcott
peteolcott
2018-11-06 19:45:10 UTC
Reply
Permalink
They are defined to be in the same language. That is why I
created Minimal Type Theory as the simple syntax for specifying HOL.
You need to make your mind up.  In a previous post you had
    ∀F ⊇ Q (∃G ∈ L(F) (G ↔ ~(F ⊢ G)))
Is it now, not 'for all F' but rather for that particular F known as Minimal Type Theory?
In another previous post you had
'"In every formal system F there does not exist a proposition G that
 is materially equivalent to a statement of its own unprovability."
∀F ∈ Formal_Systems ~∃G ∈ L(F) (G ↔ ~(F ⊢ G)))
∀F ∈ Formal_Systems ~∃G ∈ L(F) (G ↔ ~(F ⊢ G)))
∴ ~∃ Gödel_Sentence(G) in any form besides misconception.'
Is it now, not 'In every formal system F' but rather for that particular F known as Minimal Type Theory?
Minimal Type Theory (among other things) provides a very simple syntax
for specifying arbitrary levels of logic from 0 to N.

So we can restate my claim as the following:
Expression X of Language F evaluates to false in every formal system F
such that WFF(F, X) and Conventional_Semantics_For_Logical_Symbols(F).

// The following expression is named X
∀F ∈ Formal_Systems ~∃G ∈ L(F) (G ↔ ~(F ⊢ G))) --
∴ ~∃ Gödel_Sentence(G) in any form besides misconception. --

Copyright 2018 Pete Olcott
peteolcott
2018-11-07 01:56:41 UTC
Reply
Permalink
Post by peteolcott
     From where have you got the idea that there is such a thing as proof by analogy in mathematics?
What a load of horseshit. Analogies are inherently non-exhaustive. That's what makes them analogies rather than the real thing.
You would understand that I am correct
Why would I want to "understand" something that is false?
So you still think that you can define an axiom where a "cat" as a type of {dog} ?
Lots of things are possible when dealing with formal systems. You can take any existing formal system F and create a new one F' by making any non-axiomatic proposition you want from F as an axiom in F'.
If you want to restrict your formal systems in some way, you're going to have to work a LOT harder than you have been.  It'll probably take you another "thirty years", and you'll still manage to screw up the details.
(within the preexisting set of axioms that define {dog} and {cat} as having mutually exclusive properties)
In your world, cats and dogs aren't both mammals? Which ones are mammals, and which ones don't have that property?
By the way, I'm sure in the 60s, there were a lot of cats that were dogs.
∀x Bachelor(x) → ~Married(x)
∀x Bachelor(x) ⊢ ~Married(x)
You've ALMOST learned the difference between a formal system and a metalanguage. I say "almost", because I suspect you still think those two expressions belong to the same language.
EFQ
They are defined to be in the same language. That is why I
created Minimal Type Theory as the simple syntax for specifying HOL.
What do you mean by a theory being the syntax for something?  Usually, one defines syntax (using a metalanguage, say English supplemented with names for constituents of a theory T) on the way to specifying T.
To the best of my knowledge the term "Theory" of "Type Theory" is a different
sense meaning than the term "Theory" from symbolic logic.

Now that I seem to correctly understand several of the other conventional terms,
such as Mendelson formal proof and Mendelson Theorem maybe I should learn what
"theory" means in symbolic logic.

What would be the best subscript for the term {Theory} that is being discussed here:
Theory(common English)
Theory(math)
Theory(symbolic logic)
Franz Gnaedinger
2018-11-06 08:23:52 UTC
Reply
Permalink
Post by peteolcott
Copyright 2018 Pete Olcott
Peter Olcott knows the absolute and complete and total truth, he is the author
of life and creator of life, he has hundred reasons to believe that he is God,
he creates our future minds in order that we can go on existing, he is both
a human being a n d God, he is the one Creator of the Universe (claims he
made in sci.lang). In his later years Goedel tried to prove the existence of
God. He failed, but now Olcott succeeds

1) only God can dismiss a proven theorem
2) Olcott dismisses Goedel's proven theorems
3) ergo Olcott is Allgod
peteolcott
2018-11-06 18:38:07 UTC
Reply
Permalink
Post by Franz Gnaedinger
Post by peteolcott
Copyright 2018 Pete Olcott
Peter Olcott knows the absolute and complete and total truth, he is the author
of life and creator of life, he has hundred reasons to believe that he is God,
he creates our future minds in order that we can go on existing, he is both
a human being a n d God, he is the one Creator of the Universe (claims he
made in sci.lang). In his later years Goedel tried to prove the existence of
God. He failed, but now Olcott succeeds
1) only God can dismiss a proven theorem
2) Olcott dismisses Goedel's proven theorems
3) ergo Olcott is Allgod
1) Is blasphemy in that it allocates infallibility to mortal man.

I can see how you might be lead astray this way it because math
itself is infallible. The problem is that human understanding of
math has tiny little gaps here an there that hardly anyone has
ever noticed.

The only possible way that I could see these tiny little gaps
is through my system of categorically exhaustive reasoning.
DKleinecke
2018-11-06 19:23:12 UTC
Reply
Permalink
Post by peteolcott
Post by Franz Gnaedinger
Post by peteolcott
Copyright 2018 Pete Olcott
Peter Olcott knows the absolute and complete and total truth, he is the author
of life and creator of life, he has hundred reasons to believe that he is God,
he creates our future minds in order that we can go on existing, he is both
a human being a n d God, he is the one Creator of the Universe (claims he
made in sci.lang). In his later years Goedel tried to prove the existence of
God. He failed, but now Olcott succeeds
1) only God can dismiss a proven theorem
2) Olcott dismisses Goedel's proven theorems
3) ergo Olcott is Allgod
1) Is blasphemy in that it allocates infallibility to mortal man.
I can see how you might be lead astray this way it because math
itself is infallible. The problem is that human understanding of
math has tiny little gaps here an there that hardly anyone has
ever noticed.
The only possible way that I could see these tiny little gaps
is through my system of categorically exhaustive reasoning.
But almost everything you say about mathematics is,
by the standards of mathematics, incorrect. Or, as
someone once said about string theory, not coherent
enough to be wrong.
peteolcott
2018-11-06 19:54:02 UTC
Reply
Permalink
Post by DKleinecke
Post by peteolcott
Post by Franz Gnaedinger
Post by peteolcott
Copyright 2018 Pete Olcott
Peter Olcott knows the absolute and complete and total truth, he is the author
of life and creator of life, he has hundred reasons to believe that he is God,
he creates our future minds in order that we can go on existing, he is both
a human being a n d God, he is the one Creator of the Universe (claims he
made in sci.lang). In his later years Goedel tried to prove the existence of
God. He failed, but now Olcott succeeds
1) only God can dismiss a proven theorem
2) Olcott dismisses Goedel's proven theorems
3) ergo Olcott is Allgod
1) Is blasphemy in that it allocates infallibility to mortal man.
I can see how you might be lead astray this way it because math
itself is infallible. The problem is that human understanding of
math has tiny little gaps here an there that hardly anyone has
ever noticed.
The only possible way that I could see these tiny little gaps
is through my system of categorically exhaustive reasoning.
But almost everything you say about mathematics is,
by the standards of mathematics, incorrect. Or, as
someone once said about string theory, not coherent
enough to be wrong.
My largest difficulty in communicating previously was that I did not
have a deep enough understanding of the subtle nuances of the conventional
terms of the art and the conventional meaning of the logic symbols.

What I was saying about a year ago and more would have seemed quite
foolish to anyone not fully appreciating the semantic meanings that
I was attempting to express.

Now I finally have an excellent understanding of every relevant aspect
of these conventional terms and symbols, thus can finally effectively
communicate and prove my point.

My understanding of model theory is still next to nil, yet may be
able to directly show how this does not matter.

V(P)=1 is only really saying that True(P) is satisfied, likewise
V(Q)=0 only meaning that False(Q) is satisfied.
Franz Gnaedinger
2018-11-09 09:29:40 UTC
Reply
Permalink
Post by peteolcott
Copyright 2018 Pete Olcott
Peter Olcott wrote that his primary concern has always been the truth.
Following this noble maxim he dismisses proven theorems of mathematical
logic and made these claims in sci.lang: he knows the absolute and complete
and total truth, he is the author of life and creator of life, he has hundred
reasons to believe that he is God, he creates our future minds in order that
we can go on existing, he is a human being _and_ God, he is the one Creator
of the Universe. Fortunately the real creator of the world foresaw institutions
where an Allgod can find help.
peteolcott
2018-11-09 15:58:10 UTC
Reply
Permalink
Post by Franz Gnaedinger
Post by peteolcott
Copyright 2018 Pete Olcott
Peter Olcott wrote that his primary concern has always been the truth.
Following this noble maxim he dismisses proven theorems of mathematical
logic and made these claims in sci.lang: he knows the absolute and complete
and total truth, he is the author of life and creator of life, he has hundred
reasons to believe that he is God, he creates our future minds in order that
we can go on existing, he is a human being _and_ God, he is the one Creator
of the Universe. Fortunately the real creator of the world foresaw institutions
where an Allgod can find help.
Any mindless idiot can continue to mindlessly repeat:
you are wrong, you are wrong, you are wrong:

CAN ANYONE FIND ANY ACTUAL MISTAKE ???

http://liarparadox.org/index.php/2018/11/09/simplifying-the-tarski-undefinability-sentence/

http://liarparadox.org/index.php/2018/11/04/godels-1931-incompleteness-theorem-as-simple-as-possible/
Loading...