Refuting Incompleteness and Undefinability Version(15)

[peteolcott]

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]

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]

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]

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]

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]

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]

∀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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

    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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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.

[peteolcott]

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]

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]

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]

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]

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/

[Peter T. Daniels]

Post by Peter Percival
sci.lang removed

Then why am I seeing this message? (It wasn't quoted by PO.)

[peteolcott]

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]

If by theory(math) it is meant formal_system(logic) then don't overload
theory(science) with an incompatible meaning, use formal_system(logic)
instead.

I don't know what formal_system(logic) means.  Will you say?  If your correspondent used the term, why not ask what they meant?

I am not 100% sure if <is-defined-to-be>
x := y means x <is defined to be another name for> y
Also it seems that := is the most common symbol for this
type of meaning

It's one of many.  If you don't want to write
     foo is defined to mean bar
but you want to use some symbol in place of "is defined to mean" then choose one of the common ones and, if there's any possibility of misunderstanding, tell us that's what your doing.

I want the most conventional symbol that means
X <is defined to be another name for> Y

I'm still lost.

I am looking for macro substitution from computer science not
logical equivalence from math.

Does this specify infinite recursion ?
LiarParadox := ~True(LiarParadox)

Here is Tarski's version (my paraphrase is on the right):
(3) x ∉ Pr ↔ x ∈ Tr // ~Provable(x) ↔ True(x)

    foo is defined to mean bar
is different from
    foo is a name for bar.
     London is the capital of the UK.
     'London' has six letters.
that are used to explain the difference between things and their names.

I am not talking about this distinction because I am only talking about
concepts not their symbolic form of representation.

Kurt Gödel 1944
By the theory of simple types I mean the doctrine which says that the objects
of thought are divided into types, namely: individuals, properties of individuals,
relations between individuals, properties of such relations, etc., and that
sentences of the form: " a has the property φ ", " b bears the relation R to c ",
etc. are meaningless, if a, b, c, R, φ are not of types fitting together.

How many letters in the word "true" is not a question that I ever
address. How many letters in the concept of {true} ? is analogous to
asking how many feet long is the color of your car?

[Peter Percival]

Post by peteolcott

If by theory(math) it is meant formal_system(logic) then don't overload
theory(science) with an incompatible meaning, use formal_system(logic)
instead.

I don't know what formal_system(logic) means.  Will you say?  If
your correspondent used the term, why not ask what they meant?

I am not 100% sure if <is-defined-to-be>
x := y means x <is defined to be another name for> y
Also it seems that := is the most common symbol for this
type of meaning

It's one of many.  If you don't want to write
     foo is defined to mean bar
but you want to use some symbol in place of "is defined to mean"
then choose one of the common ones and, if there's any possibility
of misunderstanding, tell us that's what your doing.

I want the most conventional symbol that means
X <is defined to be another name for> Y

I'm still lost.

I am looking for macro substitution from computer science not
logical equivalence from math.
Does this specify infinite recursion ?
LiarParadox := ~True(LiarParadox)

A macro processor that sees LiarParadox will produce

~True(~True(~True(~True(~True(...)))))

until it blows its stack, won't it? (Or runs out of heap, or something.
I can't be expected to know.)

Post by peteolcott
(3) x ∉ Pr ↔ x ∈ Tr  // ~Provable(x) ↔ True(x)

     foo is defined to mean bar
is different from
     foo is a name for bar.
Did I not recently post - If you ever read an introduction to logic
      London is the capital of the UK.
      'London' has six letters.
that are used to explain the difference between things and their names.

I am not talking about this distinction because I am only talking about
concepts not their symbolic form of representation.
Kurt Gödel 1944
By the theory of simple types I mean the doctrine which says that the objects
of thought are divided into types, namely: individuals, properties of individuals,
relations between individuals, properties of such relations, etc., and that
sentences of the form: " a has the property φ ", " b bears the relation R to c ",
etc. are meaningless, if a, b, c, R, φ are not of types fitting together.
How many letters in the word "true" is not a question that I ever
address. How many letters in the concept of {true} ? is analogous to
asking how many feet long is the color of your car?

[peteolcott]

Post by Peter Percival

Post by peteolcott

If by theory(math) it is meant formal_system(logic) then don't overload
theory(science) with an incompatible meaning, use formal_system(logic)
instead.

I don't know what formal_system(logic) means.  Will you say?  If your correspondent used the term, why not ask what they meant?

I am not 100% sure if <is-defined-to-be>
x := y means x <is defined to be another name for> y
Also it seems that := is the most common symbol for this
type of meaning

It's one of many.  If you don't want to write
     foo is defined to mean bar
but you want to use some symbol in place of "is defined to mean" then choose one of the common ones and, if there's any possibility of misunderstanding, tell us that's what your doing.

I want the most conventional symbol that means
X <is defined to be another name for> Y

I'm still lost.

I am looking for macro substitution from computer science not
logical equivalence from math.
Does this specify infinite recursion ?
LiarParadox := ~True(LiarParadox)

A macro processor that sees LiarParadox will produce
~True(~True(~True(~True(~True(...)))))
until it blows its stack, won't it?  (Or runs out of heap, or something.  I can't be expected to know.)

On the other hand
LiarParadox ↔ ~True(LiarParadox)

The Prolog predicate unify_on_occurs_check/2 would see that
Logical_Equivalence(~True(LiarParadox), LiarParadox)

would have the same structure of expressions that it rejects:
?- equal(foo(Y), Y).

and simply reject LiarParadox as structurally malformed.

Copyright 2018 Pete Olcott

Clocksin and Mellish 2003, Programming in Prolog Using the ISO Standard Fifth Edition
Chapter 10 The Relation of Prolog to Logic, page 254.

[Peter Percival]

Post by peteolcott

Post by Peter Percival

Post by peteolcott

If by theory(math) it is meant formal_system(logic) then don't overload
theory(science) with an incompatible meaning, use
formal_system(logic)
instead.

I don't know what formal_system(logic) means.  Will you say?  If
your correspondent used the term, why not ask what they meant?

I am not 100% sure if <is-defined-to-be>
x := y means x <is defined to be another name for> y
Also it seems that := is the most common symbol for this
type of meaning

It's one of many.  If you don't want to write
     foo is defined to mean bar
but you want to use some symbol in place of "is defined to mean"
then choose one of the common ones and, if there's any possibility
of misunderstanding, tell us that's what your doing.

I want the most conventional symbol that means
X <is defined to be another name for> Y

I'm still lost.

I am looking for macro substitution from computer science not
logical equivalence from math.
Does this specify infinite recursion ?
LiarParadox := ~True(LiarParadox)

A macro processor that sees LiarParadox will produce
~True(~True(~True(~True(~True(...)))))
until it blows its stack, won't it?  (Or runs out of heap, or
something.  I can't be expected to know.)

On the other hand
LiarParadox ↔ ~True(LiarParadox)
The Prolog predicate unify_on_occurs_check/2 would see that
Logical_Equivalence(~True(LiarParadox), LiarParadox)
?- equal(foo(Y), Y).

Are material equivalences sufficiently like identities for what you are
claiming to make sense?

Post by peteolcott
and simply reject LiarParadox as structurally malformed.

This: ((X <-> Y) <-> Z) <-> (X <-> (Y <-> Z)) is well-formed (and even
true), this: ((X = Y) = Z) = (X = (Y = Z)) is malformed.

Post by peteolcott
Copyright 2018 Pete Olcott
Clocksin and Mellish 2003, Programming in Prolog Using the ISO Standard Fifth Edition
Chapter 10 The Relation of Prolog to Logic, page 254.

[peteolcott]

It seems you are trying to saying something about all theories F that extend Q, vis that there is a formula G in the language of F that is such that G <-> ~(F |- G).  But that is obviously false because |- is not a symbol of Q.  Your formula will not
be well-formed.

Supersets of Q that include: ⊢.

Can you either specify one such theory or name a known one?

Minimal Type Theory.

You might like to ask you correspondent, when he wrote "G <-> ~(F |- G)" (as part of some larger expression that you have, until today, reproduced numerous times incorrectly) did he intend <-> and ~ to be symbols of some formal theory (if so, which
one?) or are they just abbreviation of the English "if and only if" and "it is not the case that"?  If the latter, is s/he using an object-/meta-language distinction that you deny is necessary?
Do you think that repeatedly using the fatuous idiom "world class expert" excuses you from understanding what s/he is telling you?

I am just trying to at least fix the quantifier scope problem that EFQ brought up.

In the correct version of ∀F (F ∈ Formal_Systems  & Q ⊆ F) → ∃G ∈ L(F) (G ↔ ~(F ⊢ G)) will you want the ∀ to bind all occurrences of F?

Yes.

The set F specified on the LHS is intended to be referenced on the RHS, it is the same F on both sides.

[peteolcott]

It seems you are trying to saying something about all theories F that extend Q, vis that there is a formula G in the language of F that is such that G <-> ~(F |- G).  But that is obviously false because |- is not a symbol of Q.  Your formula will not
be well-formed.

Supersets of Q that include: ⊢.

Can you either specify one such theory or name a known one?

As soon as we hypothesize the existence of such a theory we can
∀x True(x) ↔ ⊢x

Meaning what by 'satisfiability'?
Can you define 'x is true' to mean '⊢x'?  Yes, of course you can.  But if you do so that doesn't make what Tarski has to say about truth wrong.  Why not?  Because he didn't mean by true what you mean by it.

What Tarski means by True(x) is a generic predicate that always consistently
decides when sentences of language precisely correspond to the intuitive
concept of a true sentence in a language.

The foundation of Minimal Type Theory was able to show that the concept of
true sentences can be made mathematically precise. // From my resume

[peteolcott]

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]

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]

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]

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]

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]

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]

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]

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/

[peteolcott]

I acknowledge that I have not done a very good job of this until very recently.

You should have stopped before "until".

So far the only term that I have precisely defined on the basis of existing
definitions is the term axiom.

Nope, you get that one wrong, too.

I define an axiom as any expression of (formal or natural) language that has
been expressly defined to have a Boolean property

So you're back to believing only in Boolean logic, rather than three-valued logic? You no longer believe some sentences are "wrong"?

with the value of True.

Nope, there is no inherent reason axioms must be true.

In turns out that this meaning of axiom

.... is wrong.
EFQ

Axiom(Olcott) is the fundamental basis of all truth because it is any expression
of language that has been defined to have a Boolean property assigned the value of True.
An axiom is not some true-ish thing.

https://www.britannica.com/topic/tautology
Tautology, in logic, a statement so framed that it cannot be denied
without inconsistency. Thus, “All humans are mammals” is held to
assert with regard to anything whatsoever that either it is a human
or it is not a mammal. But that universal “truth” follows not from
any facts noted about real humans but only from the actual use of
human and mammal and is thus purely a matter of definition.

When we understand that it is a fact that {cats} are not a type of {dog} it is
only because of a set of axioms(Olcott) that assign mutually exclusive properties
to {Cats} and {Dogs}.

When we know that "2 + 3 = 5" is true we know this on the basis of the axioms of
Peano Arithmetic. We don't just say that "2 + 3 = 5" is Peano axiomatic, we say
that it is true, therefore Axioms form the foundation of Truth in math.

[Franz Gnaedinger]

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 and God, he is the one Creator of the Universe, he really is
the one with the masterplan of the design of the universe (claims he made
in sci.lang). An American professoressa of the constitutional law, highly
esteemed by colleagues and students alike, married with children, suffers
from a schizophrenic disorder. She copes with her illness by occupying her
mind with complex problems - real problems, not indulging in megalomanic
delusions.

[peteolcott]

I want to assign WFF to symbolic names so that these symbolic names can be
bound to quantifiers

In HOL there can be variables that range over the class of formulae; and there is protothetic too.
Jargon: variables are bound *by* quantifiers, not *to* them.
More than just jargon: names are constants and therefore can't be bound by quantifiers.

In my simplification specifying HOL expressions using FOPL syntax
All of the names that specify a class of formula can be bound by quantifiers.

Maybe read Church, /Intro. to mathematical logic/.

I am establishing new conventions

No you're not.  You're using well-known technical terms wrongly.

int X = 55;
you are not free to correctly say that your opinion is that X != 55.
I am defining MY TERMS on the basis of adaptations to existing terms.

You resolutely refuse to define your terms.  "HOL expressions using FOPL syntax" makes no sense.  HOL has at least two kinds of quantifier: one kind ranges over a set C of individuals, the other kind ranges over the power set of C.  How does FOPL syntax
allow that?

Here is a concrete example of translating a SOL expression
into a connected hierarchy of FOL expressions.

x := y means x is defined to be another name for y

Second order logic: ∀P∀x(x ∈ P ∨ x ∉ P)
is translated to the MTT hierarchy of FOPL:
Z := (x ∈ P)
∀P∀x(Z ∨ ~Z)

Semantic interpretation connects this hierarchy in a directed acyclic graph,
thus the assigned alias names are merely temporary placeholders and are
discarded at the semantic interpretation level.

This way any level of logic can be built from FOPL syntax.

My prior example of this had typos making it incomprehensible.

Copyright Pete Olcott

[Franz Gnaedinger]

Post by peteolcott
Copyright 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 a human
being and God in personal union, he is the one Creator of the Universe, he
really is the one with the masterplan of the design of the universe (claims
he made and declarations he declared and asseverations he asserted in sci.lang).
No computer firm will employ a Goedel denyer, even noer an Allgod.

[peteolcott]

I want to assign WFF to symbolic names so that these symbolic names can be
bound to quantifiers

In HOL there can be variables that range over the class of formulae; and there is protothetic too.
Jargon: variables are bound *by* quantifiers, not *to* them.
More than just jargon: names are constants and therefore can't be bound by quantifiers.

In my simplification specifying HOL expressions using FOPL syntax
All of the names that specify a class of formula can be bound by quantifiers.

Maybe read Church, /Intro. to mathematical logic/.

I am establishing new conventions

No you're not.  You're using well-known technical terms wrongly.

int X = 55;
you are not free to correctly say that your opinion is that X != 55.

Since you added the word "opinion" here, he is free to correctly say that in his opinion, X is not 55.

I am defining MY TERMS on the basis of adaptations to existing terms.

You're lying as you don't provide the definitions you use and you don't make it clear that you are using alternative definitions.

     https://www.britannica.com/topic/tautology
     Tautology, in logic, a statement so framed that it cannot be denied
     without inconsistency. Thus, “All humans are mammals” is held to
     assert with regard to anything whatsoever that either it is a human
     or it is not a mammal. But that universal “truth” follows not from
     any facts noted about real humans but only from the actual use of
     human and mammal and is thus purely a matter of definition.
I acknowledge that I have not done a very good job of this until very recently.

Don't do yourself down.  Such is your consistency that you continue to do a very poor job.

So far the only term that I have precisely defined on the basis of existing
definitions is the term axiom.
I define an axiom as any expression of (formal or natural) language that has
been expressly defined to have a Boolean property with the value of True.

If you take "axiom" to mean that then you cannot declare wrong any facts of logic which are based on a different definition of axiom.

All of the "facts" of logic merely provide more vague definitions,
that do not contradict my further elaboration.

Since axioms are always used as the basis of inference to determine
whether or not an expression of language is satisfied in the
exact same way that true premises are used as the basis of sound
deductive reasoning for all practical purposes the axioms of symbolic
logic ARE the true premises of sound deductive inference.

It is really not that large stretch of the imagination.
If is walks like a duck, quacks like a duck, and even
lays eggs just like a duck then it would really seem to
be an actual duck.

[peteolcott]

That semantics can be exhaustively specified syntactically is one key
thing that I learned from Richard Montague's grammar of semantics.

Then you learned nothing from Montague.
EFQ

In his paper that described the Montague grammar of semantics:
(Richard Montague, 1970 ‘Universal Grammar’)
There is in my opinion no important theoretical difference between natural
languages and the artificial languages of logicians; indeed, I consider it
possible to comprehend the syntax and semantics of both kinds of languages
within a single natural and mathematically precise theory.

I saved this quote this time so I will not have to keep looking it
up every time that you show your ignorance.

The single natural and mathematically precise theory is Minimal Type Theory
which is really nothing more than a very concise and simple way to specify
this:

Kurt Gödel (1944)
By the theory of simple types I mean the doctrine which says that the objects
of thought (or, in another interpretation, the symbolic expressions) are divided
into types, namely: individuals, properties of individuals, relations between
individuals, properties of such relations, etc. (with a similar hierarchy for
extensions), and that sentences of the form: " a has the property φ ", " b bears
the relation R to c ", etc. are meaningless, if a, b, c, R, φ are not of types
fitting together.

[Peter Percival]

Post by peteolcott

That semantics can be exhaustively specified syntactically is one key
thing that I learned from Richard Montague's grammar of semantics.

Then you learned nothing from Montague.
EFQ

(Richard Montague, 1970 ‘Universal Grammar’)
There is in my opinion no important theoretical difference between natural
languages and the artificial languages of logicians; indeed, I consider it
possible to comprehend the syntax and semantics of both kinds of languages
within a single natural and mathematically precise theory.
I saved this quote this time so I will not have to keep looking it
up every time that you show your ignorance.
The single natural and mathematically precise theory is Minimal Type Theory

Supposing that Montague was right in his opinion, it does not follow
that MTT will do the job.

Post by peteolcott
which is really nothing more than a very concise and simple way to specify

[Peter T. Daniels]

Post by peteolcott
(Richard Montague, 1970 ‘Universal Grammar’)
There is in my opinion no important theoretical difference between natural
languages and the artificial languages of logicians; indeed, I consider it
possible to comprehend the syntax and semantics of both kinds of languages
within a single natural and mathematically precise theory.
I saved this quote this time so I will not have to keep looking it
up every time that you show your ignorance.

Unfortunately he then died, so he was not able to see the failure of his
hypothesis after it was taken seriously by prominent linguists for several
years.

[peteolcott]

Post by Peter T. Daniels

Post by peteolcott
(Richard Montague, 1970 ‘Universal Grammar’)
There is in my opinion no important theoretical difference between natural
languages and the artificial languages of logicians; indeed, I consider it
possible to comprehend the syntax and semantics of both kinds of languages
within a single natural and mathematically precise theory.
I saved this quote this time so I will not have to keep looking it
up every time that you show your ignorance.

Unfortunately he then died, so he was not able to see the failure of his
hypothesis after it was taken seriously by prominent linguists for several
years.

David Kleinecke has already acknowledged that this works:
http://www.cyc.com/documentation/ontologists-handbook/writing-efficient-cycl/cycl-representation-choices/

[DKleinecke]

Post by peteolcott

Post by Peter T. Daniels

Post by peteolcott
(Richard Montague, 1970 ‘Universal Grammar’)
There is in my opinion no important theoretical difference between natural
languages and the artificial languages of logicians; indeed, I consider it
possible to comprehend the syntax and semantics of both kinds of languages
within a single natural and mathematically precise theory.
I saved this quote this time so I will not have to keep looking it
up every time that you show your ignorance.

Unfortunately he then died, so he was not able to see the failure of his
hypothesis after it was taken seriously by prominent linguists for several
years.

http://www.cyc.com/documentation/ontologists-handbook/writing-efficient-cycl/cycl-representation-choices/

Please quote me accurately in the future.

I agreed that CyCorp had, in section 8.1, correctly
expounded Davidson's ideas. This has nothing to do
with Montague grammar.

[peteolcott]

Post by DKleinecke

Post by peteolcott

Post by Peter T. Daniels

Post by peteolcott
(Richard Montague, 1970 ‘Universal Grammar’)
There is in my opinion no important theoretical difference between natural
languages and the artificial languages of logicians; indeed, I consider it
possible to comprehend the syntax and semantics of both kinds of languages
within a single natural and mathematically precise theory.
I saved this quote this time so I will not have to keep looking it
up every time that you show your ignorance.

Unfortunately he then died, so he was not able to see the failure of his
hypothesis after it was taken seriously by prominent linguists for several
years.

http://www.cyc.com/documentation/ontologists-handbook/writing-efficient-cycl/cycl-representation-choices/

Please quote me accurately in the future.
I agreed that CyCorp had, in section 8.1, correctly
expounded Davidson's ideas. This has nothing to do
with Montague grammar.

You did not understand that it implements the ideas of Montague's famous quote?

In his paper that described the Montague grammar of semantics:
(Richard Montague, 1970 ‘Universal Grammar’)
There is in my opinion no important theoretical difference between natural
languages and the artificial languages of logicians; indeed, I consider it
possible to comprehend the syntax and semantics of both kinds of languages
within a single natural and mathematically precise theory.

[DKleinecke]

Post by peteolcott

Post by DKleinecke

Post by peteolcott

Post by Peter T. Daniels

Post by peteolcott
(Richard Montague, 1970 ‘Universal Grammar’)
There is in my opinion no important theoretical difference between natural
languages and the artificial languages of logicians; indeed, I consider it
possible to comprehend the syntax and semantics of both kinds of languages
within a single natural and mathematically precise theory.
I saved this quote this time so I will not have to keep looking it
up every time that you show your ignorance.

Unfortunately he then died, so he was not able to see the failure of his
hypothesis after it was taken seriously by prominent linguists for several
years.

http://www.cyc.com/documentation/ontologists-handbook/writing-efficient-cycl/cycl-representation-choices/

Please quote me accurately in the future.
I agreed that CyCorp had, in section 8.1, correctly
expounded Davidson's ideas. This has nothing to do
with Montague grammar.

You did not understand that it implements the ideas of Montague's famous quote?

I did not and I still don't. The basic point made in
section 8.1 is the same point the DEACON project
reached in 1965. See

www.computer.org/csdl/proceedings/afips/1966/5068/00/50680365.pdf

Innocent of even Chomsky much less Montague.

[peteolcott]

Post by DKleinecke

Post by peteolcott

Post by DKleinecke

Post by peteolcott

Post by Peter T. Daniels

Post by peteolcott
(Richard Montague, 1970 ‘Universal Grammar’)
There is in my opinion no important theoretical difference between natural
languages and the artificial languages of logicians; indeed, I consider it
possible to comprehend the syntax and semantics of both kinds of languages
within a single natural and mathematically precise theory.
I saved this quote this time so I will not have to keep looking it
up every time that you show your ignorance.

Unfortunately he then died, so he was not able to see the failure of his
hypothesis after it was taken seriously by prominent linguists for several
years.

http://www.cyc.com/documentation/ontologists-handbook/writing-efficient-cycl/cycl-representation-choices/

Please quote me accurately in the future.
I agreed that CyCorp had, in section 8.1, correctly
expounded Davidson's ideas. This has nothing to do
with Montague grammar.

You did not understand that it implements the ideas of Montague's famous quote?

I did not and I still don't. The basic point made in
section 8.1 is the same point the DEACON project
reached in 1965. See
www.computer.org/csdl/proceedings/afips/1966/5068/00/50680365.pdf
Innocent of even Chomsky much less Montague.

Since Davidson directly provided a specific concrete example
of what Montague referred to I don't see how you can deny this
except though the psychological rather than logical form of denial.

Montague is right it is totally obvious that Montague is proven right
and you only disagree because you don't like it that Montague is right.