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

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.

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.

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

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.

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.

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

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.

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.

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

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.

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.

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.

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

On 12/3/2023 10:44 AM, olcott wrote:
> 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.

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.

On 12/3/2023 11:10 AM, Jim Burns wrote:
> On 12/3/2023 10:44 AM, olcott wrote:
>> 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.
>
> 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.

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.

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

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.

On 12/3/23 10:44 AM, olcott wrote:
> 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.
>

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.

On 12/3/2023 1:03 PM, Jim Burns wrote:
> 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 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.

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

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

On 12/3/2023 1:03 PM, Jim Burns wrote:
> 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.
>

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/

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

On 12/3/2023 4:14 PM, Jim Burns wrote:
> 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
>
>

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.

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

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
∃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.

On 12/3/2023 9:57 PM, Jim Burns wrote:
> 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
> ∃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.
>

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.

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

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.

On 12/4/2023 8:15 AM, Jim Burns wrote:
> 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.

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.

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

On 12/4/23 5:02 PM, olcott wrote:
> On 12/4/2023 8:15 AM, Jim Burns wrote:
>> 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.
>
> One can make any idea sufficiently convoluted
> to make it incomprehensible.

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.

On 12/4/2023 8:15 AM, Jim Burns wrote:
> 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.
>
>

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)

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

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*

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