Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss

Gödel's 1931 incompleteness fails HOL

141 views
Skip to first unread message

olcott

unread,
Dec 2, 2023, 7:22:17 PM12/2/23
to
When PA is the n level of logic and metamathematics is the n+1 level of
logic in the same formal system then G <is> provable in this formal
system and incompleteness cannot exist. HOL can do this.

This sentence is not true: "This sentence is not true" is true.
The above is all there is to the Tarski Undefinability Theorem.
https://liarparadox.org/Tarski_275_276.pdf

--
Copyright 2023 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer

Richard Damon

unread,
Dec 2, 2023, 10:09:06 PM12/2/23
to
On 12/2/23 7:22 PM, olcott wrote:
> When PA is the n level of logic and metamathematics is the n+1 level of
> logic in the same formal system then G <is> provable in this formal
> system and incompleteness cannot exist. HOL can do this.

Except that incompleteness says that a given proposition that is true in
the system can't be proven in that system. Just because it is provable
in some higher power system, doesn't make that system complete.

So, you are just showing your ignorance of what you talk about, not
understanding what metalogic is actually about.

Note, you have an error in your logic, as the metamatematics of the n+1
level is a DIFFERENT (but related) formal system then the n level
system, because the meta system has additional "truthmakers" to it, that
provide information about the base system.

>
> This sentence is not true: "This sentence is not true" is true.
> The above is all there is to the Tarski Undefinability Theorem.
> https://liarparadox.org/Tarski_275_276.pdf
>

Nope. You just don't understand the proof, showing your ignorance.

What Tarski shows is that the assumption that Truth can be "defined" (in
the sense that there is a computable relationship that will tell you the
truth value of a sentence in the system) implies that ability to "prove"
that "This sentence is not true" is, in fact, true, (which implies that
it also must not be true) and thus the system is inconsistant.

olcott

unread,
Dec 2, 2023, 10:34:39 PM12/2/23
to
On 12/2/2023 6:22 PM, olcott wrote:
> When PA is the n level of logic and metamathematics is the n+1 level of
> logic in the same formal system then G <is> provable in this formal
> system and incompleteness cannot exist. HOL can do this.
>
> This sentence is not true: "This sentence is not true" is true.
> The above is all there is to the Tarski Undefinability Theorem.
> https://liarparadox.org/Tarski_275_276.pdf
>

When two formal systems are included in the same formal system
as logic levels of n and n+1 then anything expressed in the
n level of PA is provable in the n+1 level of metamathematics
and incompleteness cannot exist.

If G is expressed at the n+1 level then the n+2 level proves G.

Richard Damon

unread,
Dec 2, 2023, 11:00:39 PM12/2/23
to
On 12/2/23 10:34 PM, olcott wrote:
> On 12/2/2023 6:22 PM, olcott wrote:
>> When PA is the n level of logic and metamathematics is the n+1 level of
>> logic in the same formal system then G <is> provable in this formal
>> system and incompleteness cannot exist. HOL can do this.
>>
>> This sentence is not true: "This sentence is not true" is true.
>> The above is all there is to the Tarski Undefinability Theorem.
>> https://liarparadox.org/Tarski_275_276.pdf
>>
>
> When two formal systems are included in the same formal system
> as logic levels of n and n+1 then anything expressed in the
> n level of PA is provable in the n+1 level of metamathematics
> and incompleteness cannot exist.
>
> If G is expressed at the n+1 level then the n+2 level proves G.
>

Which means that level n was incomplete, as it didn't have enough
"logic" to prove the statement.

Note, G is expressed at the level of PA, and in the n+1 we can show that
G was true in PA, and that it was also unprofitable in PA, thus PA was
incomplete.

You just don't understand the requirements.

You also don't seem to understand how conversation works, and are just
proving yourself to be a dumb troll.

olcott

unread,
Dec 2, 2023, 11:24:00 PM12/2/23
to
On 12/2/2023 9:34 PM, olcott wrote:
> On 12/2/2023 6:22 PM, olcott wrote:
>> When PA is the n level of logic and metamathematics is the n+1 level of
>> logic in the same formal system then G <is> provable in this formal
>> system and incompleteness cannot exist. HOL can do this.
>>
>> This sentence is not true: "This sentence is not true" is true.
>> The above is all there is to the Tarski Undefinability Theorem.
>> https://liarparadox.org/Tarski_275_276.pdf
>>
>
> When two formal systems are included in the same formal system
> as logic levels of n and n+1 then anything expressed in the
> n level of PA is provable in the n+1 level of metamathematics
> and incompleteness cannot exist.
>
> If G is expressed at the n+1 level then the n+2 level proves G.
>

A formal system having an unlimited number of logic levels cannot
possibly be incomplete in the Gödel sense. What-so-ever can be
expressed at the n level of logic can be proven at the n+1 level
of logic of this same formal system.

Richard Damon

unread,
Dec 2, 2023, 11:34:15 PM12/2/23
to
On 12/2/23 11:23 PM, olcott wrote:
> On 12/2/2023 9:34 PM, olcott wrote:
>> On 12/2/2023 6:22 PM, olcott wrote:
>>> When PA is the n level of logic and metamathematics is the n+1 level of
>>> logic in the same formal system then G <is> provable in this formal
>>> system and incompleteness cannot exist. HOL can do this.
>>>
>>> This sentence is not true: "This sentence is not true" is true.
>>> The above is all there is to the Tarski Undefinability Theorem.
>>> https://liarparadox.org/Tarski_275_276.pdf
>>>
>>
>> When two formal systems are included in the same formal system
>> as logic levels of n and n+1 then anything expressed in the
>> n level of PA is provable in the n+1 level of metamathematics
>> and incompleteness cannot exist.
>>
>> If G is expressed at the n+1 level then the n+2 level proves G.
>>
>
> A formal system having an unlimited number of logic levels cannot
> possibly be incomplete in the Gödel sense. What-so-ever can be
> expressed at the n level of logic can be proven at the n+1 level
> of logic of this same formal system.
>

So you don't understand what those "logic levels" are, or what a "Formal
Logic System" is. The different levels are DIFFERENT formal systems, so
no "formal system" has multiple "logic levels".

You are just proving you don't know what a "Formal Logic System" is.


olcott

unread,
Dec 3, 2023, 12:02:12 AM12/3/23
to
On 12/2/2023 10:23 PM, olcott wrote:
> On 12/2/2023 9:34 PM, olcott wrote:
>> On 12/2/2023 6:22 PM, olcott wrote:
>>> When PA is the n level of logic and metamathematics is the n+1 level of
>>> logic in the same formal system then G <is> provable in this formal
>>> system and incompleteness cannot exist. HOL can do this.
>>>
>>> This sentence is not true: "This sentence is not true" is true.
>>> The above is all there is to the Tarski Undefinability Theorem.
>>> https://liarparadox.org/Tarski_275_276.pdf
>>>
>>
>> When two formal systems are included in the same formal system
>> as logic levels of n and n+1 then anything expressed in the
>> n level of PA is provable in the n+1 level of metamathematics
>> and incompleteness cannot exist.
>>
>> If G is expressed at the n+1 level then the n+2 level proves G.
>>
>
> A formal system having an unlimited number of logic levels cannot
> possibly be incomplete in the Gödel sense. What-so-ever can be
> expressed at the n level of logic can be proven at the n+1 level
> of logic of this same formal system.
>

HOL can have from 0 to N contiguous logic levels where N is a natural
number, yet not a fixed constant.

Richard Damon

unread,
Dec 3, 2023, 7:17:35 AM12/3/23
to
On 12/3/23 12:02 AM, olcott wrote:
> On 12/2/2023 10:23 PM, olcott wrote:
>> On 12/2/2023 9:34 PM, olcott wrote:
>>> On 12/2/2023 6:22 PM, olcott wrote:
>>>> When PA is the n level of logic and metamathematics is the n+1 level of
>>>> logic in the same formal system then G <is> provable in this formal
>>>> system and incompleteness cannot exist. HOL can do this.
>>>>
>>>> This sentence is not true: "This sentence is not true" is true.
>>>> The above is all there is to the Tarski Undefinability Theorem.
>>>> https://liarparadox.org/Tarski_275_276.pdf
>>>>
>>>
>>> When two formal systems are included in the same formal system
>>> as logic levels of n and n+1 then anything expressed in the
>>> n level of PA is provable in the n+1 level of metamathematics
>>> and incompleteness cannot exist.
>>>
>>> If G is expressed at the n+1 level then the n+2 level proves G.
>>>
>>
>> A formal system having an unlimited number of logic levels cannot
>> possibly be incomplete in the Gödel sense. What-so-ever can be
>> expressed at the n level of logic can be proven at the n+1 level
>> of logic of this same formal system.
>>
>
> HOL can have from 0 to N contiguous logic levels where N is a natural
> number, yet not a fixed constant.
>

Nope. Not in the sense that you are using logic levels.

The "level" (called "Order") in Higher Order Logic, deals with the sort
of predicate you can use. First Order Logic only allows predicates to
quantify on the variables of the logic system (there exists an x
that...), Second Order Logic allows adding quantification of
relationships (there exists an f(), such that f(x) ...).

The Levels of logic used in Tarski, are levels of meta-logic, where we
create a NEW Formal System which has all the axioms of the base level,
plus axioms about that base system that weren't derivable in the base.

This is something completely different.

Jim Burns

unread,
Dec 3, 2023, 7:46:47 AM12/3/23
to
On 12/2/2023 7:22 PM, olcott wrote:

> When PA is the n level of logic and
> metamathematics is the n+1 level of logic
> in the same formal system
> then
> G <is> provable in this formal system
> and incompleteness cannot exist.
> HOL can do this.

One PA.sentence not PA.provable
makes PA incomplete.

One PA.sentence PA.provable
does not make PA complete.

One PA.sentence HOL.provable
does not make PA complete.

One PA.sentence HOL.provable
does not make HOL complete.

One HOL.sentence HOL.provable
does not make HOL complete.

One HOL.sentence not HOL.provable
makes HOL incomplete.


This one PA.sentence
|
| PA" preceded by its PA.quotation
| is not PA.provable "PA
| preceded by its PA.quotation
| is not PA.provable.
|
makes PA incomplete.

This one HOL.sentence
|
| HOL" preceded by its HOL.quotation
| is not HOL.provable "HOL
| preceded by its HOL.quotation
| is not HOL.provable.
|
makes HOL incomplete.

> This sentence is not true:
> "This sentence is not true"
> is true.
> The above is all there is to
> the Tarski Undefinability Theorem.
> https://liarparadox.org/Tarski_275_276.pdf

| This sentence is not true
|
self-refers.

| "preceded by its quotation is not true"
| preceded by its quotation is not true.
|
does not self-refer.
It self-describes.


olcott

unread,
Dec 3, 2023, 10:44:12 AM12/3/23
to
On 12/3/2023 6:46 AM, Jim Burns wrote:
> On 12/2/2023 7:22 PM, olcott wrote:
>
>> When PA is the n level of logic and
>> metamathematics is the n+1 level of logic
>> in the same formal system
>> then
>> G <is> provable in this formal system
>> and incompleteness cannot exist.
>> HOL can do this.
>
> One PA.sentence not PA.provable
> makes PA incomplete.
>
> One PA.sentence PA.provable
> does not make PA complete.
>
> One PA.sentence HOL.provable
> does not make PA complete.
>
> One PA.sentence HOL.provable
> does not make HOL complete.
>
> One HOL.sentence HOL.provable
> does not make HOL complete.
>
> One HOL.sentence not HOL.provable
> makes HOL incomplete.
>
>

HOL can have from 0 to N contiguous logic levels where N
is a natural number, yet not a fixed constant.

This sentence cannot be proved: "This sentence cannot be proven"
can be proved.

HOL always has as many orders of logic needed so that anything
that can be specified can be proved.

Jim Burns

unread,
Dec 3, 2023, 12:10:17 PM12/3/23
to
No.
This one HOL.sentence
|
| HOL" preceded by its HOL.quotation
| is not HOL.provable "HOL
| preceded by its HOL.quotation
| is not HOL.provable.
|
can be specified.
It can't be both true and HOL.provable.

Displaying a different true sentence which
can be proved
doesn't contradict that.


olcott

unread,
Dec 3, 2023, 12:33:02 PM12/3/23
to
I never make the liar paradox like statements more convoluted than
necessary because 2000 years later the received view does not even
yet understand the simple one: This sentence is not true.

The sentence that you provided is simply rejected as incoherent.
HOL.{This sentence cannot be proven}. on the basis that it has
a cycle in its evaluation directed graph.

The version that you provided is simply a screwy way to
indirectly refer to a sentence that is isomorphic to
referring to its by its variable name.

Jim Burns

unread,
Dec 3, 2023, 2:03:33 PM12/3/23
to
On 12/3/2023 12:32 PM, olcott wrote:
> On 12/3/2023 11:10 AM, Jim Burns wrote:

>> [...]
>
> The sentence that you provided

This one HOL.sentence
|
| HOL" preceded by its HOL.quotation
| is not HOL.provable "HOL
| preceded by its HOL.quotation
| is not HOL.provable.

> is simply rejected as incoherent.
> HOL.{This sentence cannot be proven}.
> on the basis that it has
> a cycle in its evaluation directed graph.

This one HOL.sentence
|
| HOL" preceded by its HOL.quotation
| is not HOL.provable "HOL
| preceded by its HOL.quotation
| is not HOL.provable.
|
does not have a cycle in
its evaluation directed graph.

> The version that you provided

This one HOL.sentence
|
| HOL" preceded by its HOL.quotation
| is not HOL.provable "HOL
| preceded by its HOL.quotation
| is not HOL.provable.

> is simply
> a screwy way to indirectly refer to
> a sentence that is isomorphic to
> referring to its by its variable name.

Whether that is or isn't so,
the HOL.sentence I provided
meets your criterion for coherency:
no cyclic evaluation.

If the sentence I provided is true,
then it's not HOL.provable.

Therefore,
despite the existence of
various provable or incoherent sentences
which I didn't provide,
HOL is incomplete.


Richard Damon

unread,
Dec 3, 2023, 2:14:42 PM12/3/23
to
Nope, you ar making a category error by not actually understanding what
you are talking about.

"Orders" of logic are different then the meta-"Levels" of logic.

But of course, since you understand neither, you can't understand the
difference.

olcott

unread,
Dec 3, 2023, 2:24:06 PM12/3/23
to
Is rejected as semantically unsound on the basis that
it forms a cycle in the directed graph of its evaluation sequence.

It is simply another variation of the two sentence liar paradox.
The next sentence is not true.
The prior sentence is true.

"preceded by its HOL.quotation" is simply
a way to indirectly refer to a sentence by its name.

Jim Burns

unread,
Dec 3, 2023, 5:14:10 PM12/3/23
to
On 12/3/2023 2:24 PM, olcott wrote:
> On 12/3/2023 1:03 PM, Jim Burns wrote:
>> On 12/3/2023 12:32 PM, olcott wrote:

>>> The version that you provided
>>
>> This one HOL.sentence
>> |
>> | HOL" preceded by its HOL.quotation
>> | is not HOL.provable "HOL
>> | preceded by its HOL.quotation
>> | is not HOL.provable.
>>
>
> Is rejected as semantically unsound
> on the basis that
> it forms a cycle in the directed graph of
> its evaluation sequence.

Say that a hundred more times,
and it still won't be true.

We need to be able to express two properties
in our language-of-the-day for HOL
Arithmetic is sufficient for this, but
we can go further, as long as
we can still express it.

Proves(y,x)
if
y represents a proof in HOL of
a formula in HOL which x represents
then
Proves(y,x) is true. Otherwise, false.

Subst(x,y,z)
if
x represents a formula A(u) with
one variable not bound by a quantifier (free)
and z represents A(y)
AKA A(u) with y substituted for
free occurrences of u in A(u)
then
Subst(x,y,z) is true. Otherwise, false.

Subst(x,y,z) doesn't get much attention,
I guess. It seems to me to be
pretty much guaranteed to exist
if predicate Proves(y,x) exists

But Subst(x,y,z) is how we get
"preceded by its quotation is not provable"
to be preceded by its quotation.
These numbers representing formulas
the same as quotations:
things representing speech acts.

∃y(Subst(x,x,y) ∧ ¬∃z:Proves(z,y)))
is the HOL.predicate meaning
| x represents
| a formula A(u) such that,
| for A(x), represented here by y
| no proof, represented here by z,
| exists

For convenience, refer to
∃y(Subst(x,x,y) ∧ ¬∃z:Proves(z,y)))
as G(x)

Represent (ie, quote) G(x) as a number g
G(g) is a certain long arithmetical formula

G(g) _means_
| HOL" preceded by its HOL.quotation
| is not HOL.provable "HOL
| preceded by its HOL.quotation
| is not HOL.provable.

If G(g) is true, G(g) is not provable,
and not all true sentence of HOL
are provable.

> "preceded by its HOL.quotation" is simply
> a way to indirectly refer to a sentence
> by its name.

No.
Your "proof" that that's so
is to
swap out G(g) and put something else in.

https://en.wikipedia.org/wiki/Straw_man


olcott

unread,
Dec 3, 2023, 5:48:45 PM12/3/23
to
On 12/3/2023 1:03 PM, Jim Burns wrote:
https://en.wikipedia.org/wiki/Quine%27s_paradox
A convoluted mess that is indirectly rather than directly
self-referential.

The author of the paradox made the ridiculously stupid mistake of
not understanding that the term bachelor is defined in terms of
unmarried male yet did this so convincingly that most people to
this day reject the notion of epistemic foundationalism.
https://iep.utm.edu/quine-an/

olcott

unread,
Dec 3, 2023, 5:53:23 PM12/3/23
to
Whenever any proof contains cycles in its directed graph
it is semantically unsound and must be rejected. Otherwise
an expression of language is provable or untrue. A proof
is a directed path from the leaves of a tree to its root.

Jim Burns

unread,
Dec 3, 2023, 10:57:41 PM12/3/23
to
On 12/3/2023 5:53 PM, olcott wrote:
> On 12/3/2023 4:14 PM, Jim Burns wrote:

>> We need to be able to express two properties
>> in our language-of-the-day for HOL
>> Arithmetic is sufficient for this, but
>> we can go further, as long as
>> we can still express it.
>>
>> Proves(y,x)
>> if
>> y represents a proof in HOL of
>> a formula in HOL which x represents
>> then
>> Proves(y,x) is true. Otherwise, false.
>>
>> Subst(x,y,z)
>> if
>> x represents a formula A(u) with
>> one variable not bound by a quantifier (free)
>> and z represents A(y)
>> AKA A(u) with y substituted for
>> free occurrences of u in A(u)
>> then
>> Subst(x,y,z) is true. Otherwise, false.

> Whenever any proof contains cycles in
> its directed graph
> it is semantically unsound and must be rejected.

Do you think there are cycles in
Proves(y,x) or Subst(x,y,z) ?

If yes, why do you think that?

If no,
are there cycles in
∃y(Subst(x,x,y) ∧ ¬∃z:Proves(z,y)))
?

What cycles?

Note that

olcott

unread,
Dec 4, 2023, 12:01:15 AM12/4/23
to
https://en.wikipedia.org/wiki/Quine%27s_paradox
A convoluted mess that is indirectly rather than directly
self-referential.

The statement "'yields falsehood when preceded by its quotation'
yields falsehood when preceded by its quotation" is false.

In other words, the sentence implies that it is false, which is
paradoxical—for if it is false, what it states is in fact true.

*Thus proving a cycle in its evaluation graph*
All proves are directed paths from leaves to a root.

Jim Burns

unread,
Dec 4, 2023, 9:15:39 AM12/4/23
to
On 12/4/2023 12:01 AM, olcott wrote:
> On 12/3/2023 9:57 PM, Jim Burns wrote:

>> [...]
>
> https://en.wikipedia.org/wiki/Quine%27s_paradox
> A convoluted mess that
> is indirectly rather than directly
> self-referential.
>
> | The statement
> | "'yields falsehood when preceded by its quotation'
> | yields falsehood when preceded by its quotation"
> | is false.

G(x) :⇔ ∃y(Subst(x,x,y) ∧ ¬∃z:STProves(z,y)))

ST is: Empty.Set, Adjunct, Extensionality.

h := "H(x)"

G(h) means
| H(x) preceded by its quotation
| is not ST.provable.

g := "G(x)" ≠ "G(g)"

G(g) means
| G(x) preceded by its quotation
| is not ST.provable.

!
G(g) is G(x) preceded by its quotation.
or,
being cute,
| "preceded by its quotation
| is not ST.provable"
| preceded by its quotation
| is not ST.provable.

If G(g) is true, G(g) is not ST.provable.
g refers to G(x) not G(g)

> | In other words,
> | the sentence implies that it is false,

G(g) implies that G(g) is not ST.provable.
false ≠ not ST.provable

> | which is paradoxical
> | —for if it is false,
> | what it states is in fact true.

Incomplete ST is not paradoxical,
not even if you say it is
a hundred times.

> *Thus proving a cycle in its evaluation graph*

G(g)
Show me a cycle.

> All proves are directed paths
> from leaves to a root.

...which is what I've been saying,
calling the root
description of the topic-of-the-day and
calling the leaves
not-first-false claims augmenting
the description.

The finiteness of paths from leaves
back to root is implicit in
their being attached.


olcott

unread,
Dec 4, 2023, 5:02:59 PM12/4/23
to
One can make any idea sufficiently convoluted
to make it incomprehensible.

When one knows the foundation of formal proofs always
involves a directed path from the leaves of a tree
to its root then one has the basis to untangle the
fundamental nature of any formal proof once it has
been translated into its directed graph form.

...14 Every epistemological antinomy can likewise be used
for a similar undecidability proof...(Gödel 1931:43-44)

When it is understood that an epistemological antinomy
is merely a self-contradictory expression of language
then the above quote conclusively proves that Gödel had a
fundamental misconception about the way the formal proofs
actually work.

It is far too ridiculously stupid to believe that anyone
ever truly believed that a formal system must be able
to prove any self-contradictory expression of language.
Thus the Gödel proof becomes the Gödel ruse.

Richard Damon

unread,
Dec 4, 2023, 6:41:56 PM12/4/23
to
Which doesn't seem too hard for you. You seem to be unable to understand
the simple straight forward ideas.

>
> When one knows the foundation of formal proofs always
> involves a directed path from the leaves of a tree
> to its root then one has the basis to untangle the
> fundamental nature of any formal proof once it has
> been translated into its directed graph form.

Yes, any statement that can't be traced back by a sequence of steps
(possibly infinite) to the truth-makers of the system, can't be true.

>
> ...14 Every epistemological antinomy can likewise be used
> for a similar undecidability proof...(Gödel 1931:43-44)
>

Which you still don't understand what he means, and thus you show your
utter ignroance.

> When it is understood that an epistemological antinomy
> is merely a self-contradictory expression of language
> then the above quote conclusively proves that Gödel had a
> fundamental misconception about the way the formal proofs
> actually work.

Which, since he NEVER claimed that the epistemological antinomy actually
had a truth value, or even directly used it as a statement in the Theory
(or meta-theory) is irrelevent.

Your repeating that statement, after this has been pointed out to you,
just shows your stupidity.

>
> It is far too ridiculously stupid to believe that anyone
> ever truly believed that a formal system must be able
> to prove any self-contradictory expression of language.
> Thus the Gödel proof becomes the Gödel ruse.
>

And you seem to be the only one who thinks that is what was done, so YOU
are the stupid one.

And too ignorant to understand the actual truth.

olcott

unread,
Dec 4, 2023, 7:08:29 PM12/4/23
to
On 12/4/2023 8:15 AM, Jim Burns wrote:
When we boil Gödel's 75 levels of indirection down to what he
is expressing in a language woefully insufficiently expressive
to say this he is saying:

...We are therefore confronted with a proposition which asserts its own
unprovability. 15 ...(Gödel 1931:43-44)

This does have a cycle---> G := (F ⊬ G)

olcott

unread,
Dec 4, 2023, 7:12:24 PM12/4/23
to
On 12/2/2023 6:22 PM, olcott wrote:
> When PA is the n level of logic and metamathematics is the n+1 level of
> logic in the same formal system then G <is> provable in this formal
> system and incompleteness cannot exist. HOL can do this.
>
> This sentence is not true: "This sentence is not true" is true.
> The above is all there is to the Tarski Undefinability Theorem.
> https://liarparadox.org/Tarski_275_276.pdf
>

...14 Every epistemological antinomy can likewise be used
for a similar undecidability proof...(Gödel 1931:43-44)

Dishonest people can "interpret" this as saying everyone
knows that no one can ever base any formal proof on any
epistemological antinomy.

*the direct opposite of what he actually says*

olcott

unread,
Dec 4, 2023, 7:47:17 PM12/4/23
to
On 12/4/2023 6:12 PM, olcott wrote:
> On 12/2/2023 6:22 PM, olcott wrote:
>> When PA is the n level of logic and metamathematics is the n+1 level of
>> logic in the same formal system then G <is> provable in this formal
>> system and incompleteness cannot exist. HOL can do this.
>>
>> This sentence is not true: "This sentence is not true" is true.
>> The above is all there is to the Tarski Undefinability Theorem.
>> https://liarparadox.org/Tarski_275_276.pdf
>>
>
> ...14 Every epistemological antinomy can likewise be used
> for a similar undecidability proof...(Gödel 1931:43-44)
>
> Dishonest people can "interpret" this as saying everyone
> knows that no one can ever base any formal proof on any
> epistemological antinomy.
>
> *the direct opposite of what he actually says*
>

If
epistemological antinomies are not members of most Formal Systems Language.

Then Gödel was that much more stupid for saying this.

Jim Burns

unread,
Dec 4, 2023, 7:49:14 PM12/4/23
to
On 12/4/2023 5:02 PM, olcott wrote:
> On 12/4/2023 8:15 AM, Jim Burns wrote:
>> On 12/4/2023 12:01 AM, olcott wrote:

>>> *Thus proving a cycle in its evaluation graph*
>>
>> G(g)
>> Show me a cycle.

> One can make any idea sufficiently convoluted
> to make it incomprehensible.

I can try to make each step more comprehensible,
and take more, shorter steps.

Be aware that there may be a trade-off, though.
More short steps may well be less comprehensible
than fewer broad sweeps which clue one in on
how to think about this.

if
Subst("H(u)","H(u)",y)
is true, then
y = "H("H(u)")"

if
¬∃z:Provesˢᵗ(z,"H("H(u)")")
is true, then
H("H(u)") is not ST.provable.

if
∃y(Subst("H(u)","H(u)",y) ∧ ¬∃z:Provesˢᵗ(z,y)))
is true, then
y = "H("H(u)")" exists and
"H("H(u)") is not ST.provable

Abbreviate
G(u) := ∃y(Subst(u,u,y) ∧ ¬∃z:Provesˢᵗ(z,y)))

if
G("H(u)")
is true, then
y = "H("H(u)")" exists and
H("H(u)") is not ST.provable

if
G("G(u)")
is true, then
y = "G("G(u)")" exists and
G("G(u)") is not ST.provable


tl;dr
if G("G(u)") is true
then G("G(u)") is not ST.provable


olcott

unread,
Dec 4, 2023, 8:00:16 PM12/4/23
to
Until you get down to "G is unprovable in F"
we cannot build its proof tree.

Richard Damon

unread,
Dec 4, 2023, 8:44:07 PM12/4/23
to
On 12/4/23 7:47 PM, olcott wrote:
> On 12/4/2023 6:12 PM, olcott wrote:
>> On 12/2/2023 6:22 PM, olcott wrote:
>>> When PA is the n level of logic and metamathematics is the n+1 level of
>>> logic in the same formal system then G <is> provable in this formal
>>> system and incompleteness cannot exist. HOL can do this.
>>>
>>> This sentence is not true: "This sentence is not true" is true.
>>> The above is all there is to the Tarski Undefinability Theorem.
>>> https://liarparadox.org/Tarski_275_276.pdf
>>>
>>
>> ...14 Every epistemological antinomy can likewise be used
>> for a similar undecidability proof...(Gödel 1931:43-44)
>>
>> Dishonest people can "interpret" this as saying everyone
>> knows that no one can ever base any formal proof on any
>> epistemological antinomy.
>>
>> *the direct opposite of what he actually says*
>>
>
> If
> epistemological antinomies are not members of most Formal Systems Language.
>
> Then Gödel was that much more stupid for saying this.

He never said the epistemological antinomy was a member of the Formal
System Language.

Try to show where he did.

You are just apparently too stupid to understand wha the is saying,

Richard Damon

unread,
Dec 4, 2023, 8:44:10 PM12/4/23
to
On 12/4/23 7:12 PM, olcott wrote:
> On 12/2/2023 6:22 PM, olcott wrote:
>> When PA is the n level of logic and metamathematics is the n+1 level of
>> logic in the same formal system then G <is> provable in this formal
>> system and incompleteness cannot exist. HOL can do this.
>>
>> This sentence is not true: "This sentence is not true" is true.
>> The above is all there is to the Tarski Undefinability Theorem.
>> https://liarparadox.org/Tarski_275_276.pdf
>>
>
> ...14 Every epistemological antinomy can likewise be used
> for a similar undecidability proof...(Gödel 1931:43-44)
>
> Dishonest people can "interpret" this as saying everyone
> knows that no one can ever base any formal proof on any
> epistemological antinomy.
>
> *the direct opposite of what he actually says*
>

So, you are agreing that your own "proof" is incorrect, as you can't
base a proof on an epistemological antinomy, which you just did (at
least to a similar degree as Godel did).

Richard Damon

unread,
Dec 4, 2023, 8:44:12 PM12/4/23
to
Which you still don't understand what he is saying.

> This does have a cycle---> G := (F ⊬ G)
>

Which isn't what his G is, so you are just proving yourself to be a bald
face liar.

If you disagree, show where he ACTUALLY SAYS That is what G is.

If you quote that statement again, and don't show how its context
actually means what you claim, you will just contionuie to prove
yourself to be just a stupid liar.

Richard Damon

unread,
Dec 4, 2023, 8:44:14 PM12/4/23
to
Except that since that ISN'T the statment of G, we don't need that
statement.

The statement of G is: "There does not exist a Natural Number g that
statisfies <a particular Primative Recursive Relationship>"

There exist a proof tree for that (which is infinite in length) in F,
since that relationship can be computed for every Natural Number, and it
turns out that all the answers are that none of the numbers satisfies
the relationship. Thus, the statement IS true.

The fact that none of the numbers satisfies the relationship can't be
determined in F, except by testing every number individually, which,
because there is an infinite number of numbers, says that can't be the
needed finite proof.

It DOES turn out that in Meta-F, because of its additional knowledge
about the Primitive Recursive Relationship, we can prove that there, in
fact, is no number that matches the relationship, and by the nature of
the meta-relationship between F and meta-F, we establish that it also
must be true in F itself (because the relationship doesn't change).

So, we do have the tree in F, but it is infinite, so not a proof (since
the incompleteness thereom is for Formal System, which as true for most
normal systems, define "Proofs" as FINITE arguments.


Jim Burns

unread,
Dec 5, 2023, 12:52:38 PM12/5/23
to
On 12/4/2023 8:44 PM, Richard Damon wrote:
> On 12/4/23 8:00 PM, olcott wrote:
>> On 12/4/2023 6:49 PM, Jim Burns wrote:

>>> tl;dr
>>> if G("G(u)") is true
>>> then G("G(u)") is not ST.provable

ST has {}, x∪{y}, and set equality.

>> Until you get down to "G is unprovable in F"
>> we cannot build its proof tree.
>
> Except that since that ISN'T the statment of G,
> we don't need that statement.
>
> The statement of G is:
> "There does not exist
> a Natural Number g that statisfies
> <a particular Primative Recursive Relationship>"
>
> There exist a proof tree for that
> (which is infinite in length) in F,
> since that relationship can be computed
> for every Natural Number,
> and it turns out that
> all the answers are that
> none of the numbers satisfies the relationship.
> Thus, the statement IS true.
>
> The fact that
> none of the numbers satisfies the relationship
> can't be determined in F, except by
> testing every number individually, which,
> because there is an infinite number of numbers,
> says that can't be the needed finite proof.

What is F ?
Is F True Arithmetic?
https://en.wikipedia.org/wiki/True_arithmetic

True Arithmetic takes infinitely-many sentences
as axioms. True Arithmetic is not a counter-
example to Gödel's reasoning.

What Olcott wants still seems to be a
massive-database of all human knowledge,
complete, of course, and
PO sees Gödel's reasoning as what prevents that,
somehow, and
he sees that complete massive-database
as essential to True AI and
True AI as essential to humanity.

I do not guarantee that my recollection is
100% correct or thoroughly up-to-date.

However, assuming IRC,
True Arithmetic does not serve Olcott's purpose
because
the most massively massive of massive-databases
is still finite, unlike True Arithmetic.

However,
I'm not sure what F means here.


olcott

unread,
Dec 5, 2023, 2:30:40 PM12/5/23
to
∀L ∈ Formal_System ∀x ∈ Language(L)
True(L,x) ≡ (T ⊢ x)
False(L,x) ≡ (T ⊢ ¬x)
Eliminates Tarski undefinability and Gödel incompleteness and forces the
concept of truth in math and logic to conform to the way that it works
everywhere else. True(x) ≡ (⊢ x)

The only way that we know that "cats are animals" is true is the
connection from the above expression to the definition of {cats} and
{animals}.

The lack of inference steps from axioms to an expression simply means
untrue. Incomplete(L) is merely a terribly misleading euphemism for
~True(L,x).

Jim Burns

unread,
Dec 5, 2023, 2:58:59 PM12/5/23
to
On 12/5/2023 2:30 PM, olcott wrote:
> On 12/5/2023 11:52 AM, Jim Burns wrote:
>> On 12/4/2023 8:44 PM, Richard Damon wrote:
>>> On 12/4/23 8:00 PM, olcott wrote:
>>>> On 12/4/2023 6:49 PM, Jim Burns wrote:

>>>>> tl;dr
>>>>> if G("G(u)") is true
>>>>> then G("G(u)") is not ST.provable
>>
>> ST has {}, x∪{y}, and set equality.
>>
>>>> Until you get down to "G is unprovable in F"
>>>> we cannot build its proof tree.

>> he sees that complete massive-database
>> as essential to True AI  and
>> True AI as essential to humanity.
>
> ∀L ∈ Formal_System ∀x ∈ Language(L)
> True(L,x) ≡ (T ⊢ x)
> False(L,x) ≡ (T ⊢ ¬x)

What is F ?

Do I have your motivation correct?


olcott

unread,
Dec 5, 2023, 3:09:43 PM12/5/23
to
F is the formal system that encodes Gödel’s G
https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom

Jim Burns

unread,
Dec 5, 2023, 4:29:02 PM12/5/23
to
On 12/5/2023 3:09 PM, olcott wrote:
> On 12/5/2023 1:58 PM, Jim Burns wrote:
>> On 12/5/2023 2:30 PM, olcott wrote:
>>> On 12/5/2023 11:52 AM, Jim Burns wrote:
>>>> On 12/4/2023 8:44 PM, Richard Damon wrote:
>>>>> On 12/4/23 8:00 PM, olcott wrote:
>>>>>> On 12/4/2023 6:49 PM, Jim Burns wrote:

>>>>>>> tl;dr
>>>>>>> if G("G(u)") is true
>>>>>>> then G("G(u)") is not ST.provable
>>>>
>>>> ST has {}, x∪{y}, and set equality.

>>>>>> Until you get down to
>>>>>> "G is unprovable in F"
>>>>>> we cannot build its proof tree.

>> What is F ?

> F is the formal system that encodes Gödel’s G
> https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom

Thank you.

IIRC, the 1931 paper calls it P.
It is(?) a variation on the system PM in
_Principia Mathematica_

I'm not complaining about your calling it F
I just trying to to understand you.

I'm working with a much smaller axiom set,
the one for ST: {}, x∪{y}, and set equality.

ST is the system which I want to prove is
incomplete or inconsistent.

ST is still an important result, as small as
it is, because it is straightforward to
generalize the proof of ST's incompleteness
to a proof for systems which ST can describe.
And what ST can describe is Vast.

I know: that's not exactly how Godel's proof
goes. But the important thing is my proof goes.
My hope is that, shown multiple versions, you
will be able to triangulate on why it goes.

>>>> he sees that complete massive-database
>>>> as essential to True AI and
>>>> True AI as essential to humanity.
>>>
>>> ∀L ∈ Formal_System ∀x ∈ Language(L)
>>> True(L,x) ≡ (T ⊢ x)
>>> False(L,x) ≡ (T ⊢ ¬x)

olcott

unread,
Dec 5, 2023, 5:29:44 PM12/5/23
to
Eliminates Tarski undefinability and Gödel incompleteness and forces the
concept of truth in math and logic to conform to the way that it works
everywhere else in the body of human knowledge: True(x) ≡ (⊢ x)

This makes it possible for a formal axiomatic system to eventually
get on social media and argue against the two most dangerous lies
about election fraud and climate change at every language level so
that the liars look like ridiculous fools even to themselves.

When everyone in the world believes that there is no objective
and consistent measure of True(x) (Tarski proof) this is impossible.

The reasonably possible alternative is that humanity becomes
extinct simply because some people wanted to chase after one
more dollar bill.

My paper bypasses most of the climate change lies by anchoring
itself in direct measurements of CO2 for the last 800,000 years,
These direct measurements cannot be biased.

My paper shows several different measure of a huge spike in CO2 since
1950. The next fastest spike in 800,000 years took 7,500 years.

Severe anthropogenic climate change proven entirely with verifiable facts

https://www.researchgate.net/publication/336568434_Severe_anthropogenic_climate_change_proven_entirely_with_verifiable_facts

Richard Damon

unread,
Dec 5, 2023, 6:39:46 PM12/5/23
to
On 12/5/23 2:30 PM, olcott wrote:

> ∀L ∈ Formal_System ∀x ∈ Language(L)
> True(L,x) ≡ (T ⊢ x)
> False(L,x) ≡ (T ⊢ ¬x)
> Eliminates Tarski undefinability and Gödel incompleteness and forces the
> concept of truth in math and logic to conform to the way that it works
> everywhere else. True(x) ≡ (⊢ x)
>
> The only way that we know that "cats are animals" is true is the
> connection from the above expression to the definition of {cats} and
> {animals}.
>
> The lack of inference steps from axioms to an expression simply means
> untrue. Incomplete(L) is merely a terribly misleading euphemism for
> ~True(L,x).
>

And means that we can't have the Natural Numbers or anything higher.

So, you are just defining that Your idea of logic is too small to be useful.

Prove otherwise.

(Hint, if you have the Natural Numbers, then Godel's proof applies, and
proves there is either a statement that is True but not Provable, or
your system is inconsistent)

This just goes back your you lack of understand of how logic actually works.

Note, it also means you don't even know the meaning of the word "True"
in Natural Language, as things can be "True" even if not provable.

They can't be "Known True", but they can be "True"

You don't seem to understand the difference, probably because you don't
understand what Knowledge is.

Richard Damon

unread,
Dec 5, 2023, 9:27:03 PM12/5/23
to
F is the name of the Logic System used in the version of Godel's paper
that Olcott is using to (mis)understand Godel's proof. In F, we get a
statement of the form that G is the assertion that there does not exist
a Natuaral Number g that satisfies a particular Primative Recursive
Relationship. This relationship being derived in a meta-system of F that
enumerates the fundamental properties in F, and in which an encoding of
statements to numbers is defined, and the relationship is a Proof Tester
that accepts a number (and only those numbers) that encode a valid proof
of the statement G.

He seems to have a problem with the fact that SOME truths can't be
proven, and somehow thinks that means that this allows untruths to be
claimed as truth.

He seems to want there to be a massive database of all knowledge, and
then that will produce a list of everything that is actually True and
False, and thus somehow make lies go away. The irony is he atually uses
the methodology of the "fake news" crowd to try to push his idea to be
used to eliminate "fake news", because he just doesn't understand

Jim Burns

unread,
Dec 6, 2023, 12:21:54 PM12/6/23
to
On 12/5/2023 9:26 PM, Richard Damon wrote:
> On 12/5/23 12:52 PM, Jim Burns wrote:
>> On 12/4/2023 8:44 PM, Richard Damon wrote:
>>> On 12/4/23 8:00 PM, olcott wrote:
>>>> On 12/4/2023 6:49 PM, Jim Burns wrote:

>>>>> tl;dr
>>>>> if G("G(u)") is true
>>>>> then G("G(u)") is not ST.provable

>>>> Until you get down to
>>>> "G is unprovable in F"
>>>> we cannot build its proof tree.

>>> There exist a proof tree for that
>>> (which is infinite in length) in F,

>> However,
>> I'm not sure what F means here.
>
> F is the name of the Logic System used in
> the version of Godel's paper that
> Olcott is using to (mis)understand
> Godel's proof.
> In F,
> we get a statement of the form that
> G is the assertion that
> there does not exist
> a Natuaral Number g that satisfies
> a particular Primative Recursive Relationship.
> This relationship being derived in
> a meta-system of F that enumerates
> the fundamental properties in F,
> and in which
> an encoding of statements to numbers
> is defined,
> and the relationship is
> a Proof Tester that accepts
> a number (and only those numbers) that
> encode
> a valid proof of the statement G.

Thank you.

I hope you don't mind
my screwing around with your whitespace.
I'm experimenting with
prettyprinting natural language
in a manner intended to be similar to
prettyprinting computer code.

It seems to me that
natural language would benefit even more
from prettyprinting than code does.
The semantic graphs of natural language
can be at least as tangled as (good) code, but
we are expected to chalk the lines
with only a handful of pronouns instead of
unlimited-many variable names.

Anyway, thank you for answering my question.

> He seems to have a problem with the fact that
> SOME truths can't be proven, and
> somehow thinks that means that
> this allows untruths to be claimed as truth.

I've seen this syndrome elsewhere, as well.
Maybe quantifier dyslexia?

> He seems to want there to be
> a massive database of all knowledge,
> and then that will produce a list of
> everything that is actually True and False,
> and thus somehow
> make lies go away.
> The irony is
> he atually uses the methodology of
> the "fake news" crowd to try to push
> his idea to be used to eliminate "fake news",
> because he just doesn't understand

<sigh>


olcott

unread,
Dec 6, 2023, 2:08:55 PM12/6/23
to
Tarski incorrectly "proved" that there cannot be any
objective measure of True(x) that works consistently.
Whereas True(x) ≡ (⊢ x) does work consistently for
the entire body of analytical knowledge.

It includes everything known to be true on the basis
of its meaning and excludes unknown truths such as
the truth (or falsity) of the Goldbach conjecture.

Incomplete(L) is merely a terribly misleading euphemism for ~True(L,x).

...14 Every epistemological antinomy can likewise be used
for a similar undecidability proof...(Gödel 1931:43-44)

The most important thing that True(L,x) ≡ (L ⊢ x) excludes
are epistemological antinomies which form the essential
basis of Tarski's proof.

https://liarparadox.org/Tarski_275_276.pdf
(3) x ∉ Provable if and only if x ∈ True.
That is the false assumption step of the Tarski proof.

As soon as humans accept the correct measure of True(x)
then we can manually create formal proofs of English
statements. Until then all opinions including dangerous
lies are incorrectly thought to carry the same weight.

Jim Burns

unread,
Dec 6, 2023, 3:33:19 PM12/6/23