olcott <polcott2@gmail.com> writes:

> On 5/2/2022 9:21 PM, Ben wrote:
>> olcott <polcott2@gmail.com> writes:
>>
>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>
>>>>> Thanks for confirmation, that's what exactly what I was trying to tell
>>>>> to topic poster in one of my previous posts. Prolog in it's bare form
>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>
>>>>> If you want to deal with such problems maybe it is better to use Coq
>>>>> theorem prover, I've never used it by myself, but it looks like one of
>>>>> the best proving assistants out there.
>>>>
>>>> And indeed there is a fully formalised proof of GIT in Coq (though I
>>>> think it's the slightly tighter Gödel-Rosser version).
>>>
>>> It is true that G is not provable.
>> G is provable. Proofs abound. I was pointing out one in a proper proof
>> assistant, Coq.
>
> It is OK that you are not a math guy.

You are not a math guy. I am.

> If you were a math guy you would understand that if G is provable then
> that makes Gödel totally wrong. G is not Gödel's theorem, it is a key
> element of his theorem.

No. G is provable. Though I did make a mistake -- the link was to a
proof of G-RIT not G.

How are you getting on with E and specifying P? Have you given up?

--
Ben.
"le génie humain a des limites, quand la bêtise humaine n’en a pas"
Alexandre Dumas (fils)

On 5/3/2022 3:46 AM, Aleksy Grabowski wrote:
> On 5/3/22 01:43, Ben wrote:
>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>
>>>> IF you are defining that your logic system is limited to what Prolog
>>>> can "Prove", that is fine. Just realize that you have just defined
>>>> that your
>>>> logic system can't handle a lot of the real problems in the world,
>>>> and in particular, it is very limited in the mathematics it can handle.
>>>> I am pretty sure that Prolog is NOT up to handling the logic needed to
>>>> handle the mathematics needed to express Godel's G, or the Halting
>>>> Problem.
>>>> Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
>>>> have only proven that your limited logic system can't reach them in
>>>> expressibility.
>>>
>>> Thanks for confirmation, that's what exactly what I was trying to tell
>>> to topic poster in one of my previous posts. Prolog in it's bare form
>>> is a bad theorem solver. It wasn't designed a such.
>>>
>>> If you want to deal with such problems maybe it is better to use Coq
>>> theorem prover, I've never used it by myself, but it looks like one of
>>> the best proving assistants out there.
>>
>> And indeed there is a fully formalised proof of GIT in Coq (though I
>> think it's the slightly tighter Gödel-Rosser version).
>>
>
> Just for a reference here is the link to that proof:
> http://r6.ca/Goedel/goedel1.html
>
> Sadly I can't understand it and comment on it, so I just leave it as is.
>

Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).

Incomplete T means that there exists a φ such that φ is not provable or
refutable in formal system T.

It is true that Gödel's G meets this definition of incompleteness. The
problem is that the mathematical definition of incompleteness doesn't
screen out semantically incorrect expressions of language, it simply
assumes they the do not exist.

This is very very easy to fix:

∀T ∈ formal_systems
∀φ ∈ expression_of_language_T
(Incorrect(φ) ↔ ((T ⊬ φ) ∧ (T ⊬ ¬φ)))

The above screens out expressions of language that are not logic
sentences / truth bearers.

https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)#:~:text=In%20mathematical%20logic%2C%20a%20sentence,must%20be%20true%20or%20false.

Prolog detects [and rejects] pathological self reference in the Gödel
sentence
https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence

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

On 2022-05-02 18:57, olcott wrote:
> On 5/2/2022 6:43 PM, Ben wrote:
>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>
>>>> IF you are defining that your logic system is limited to what Prolog
>>>> can "Prove", that is fine. Just realize that you have just defined
>>>> that your
>>>> logic system can't handle a lot of the real problems in the world,
>>>> and in particular, it is very limited in the mathematics it can handle.
>>>> I am pretty sure that Prolog is NOT up to handling the logic needed to
>>>> handle the mathematics needed to express Godel's G, or the Halting
>>>> Problem.
>>>> Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
>>>> have only proven that your limited logic system can't reach them in
>>>> expressibility.
>>>
>>> Thanks for confirmation, that's what exactly what I was trying to tell
>>> to topic poster in one of my previous posts. Prolog in it's bare form
>>> is a bad theorem solver. It wasn't designed a such.
>>>
>>> If you want to deal with such problems maybe it is better to use Coq
>>> theorem prover, I've never used it by myself, but it looks like one of
>>> the best proving assistants out there.
>>
>> And indeed there is a fully formalised proof of GIT in Coq (though I
>> think it's the slightly tighter Gödel-Rosser version).
>>
>
> It is true that G is not provable. G is not provable because it is
> semantically incorrect in the exactly same way that the Liar Paradox is
> semantically incorrect.
>
> Gödel says:
> 14 Every epistemological antinomy can likewise be used for a similar
> undecidability proof
>
> André denied this six times yesterday
> The Liar Paradox is an epistemological antinomy, thus can likewise be
> used for a similar undecidability proof.

No. The Liar can be used to construct an *identical* proof. Other
antinomies could be used for similar proofs. He's already talking about
The Liar.

> Which means that the Liar Paradox is sufficiently equivalent to Gödel's
> G. Which means if the basic mechanism of epistemological antinomy is
> shown to be semantically incorrect then Gödel's G is shown to be
> semantically incorrect.

You have some serious reading comprehension problems. I never denied the
things Gödel wrote. I denied your conclusion because it does not follow.

Gödel starts by claiming there is a close relationship (*not*
equivalence) between one particular antinomy, The Liar, and his G.

He then states that similar proofs could be constructed using any antinomy.

That entails that other antinomies could be used to construct similar
proofs involving a similar close relation (again, *not* equivalence).

Gödel never claims *any* antinomy is equivalent to his G. Merely that a
close relationship holds.

And all my comments concerned exactly what that relationship is.

André

--
To email remove 'invalid' & replace 'gm' with well known Google mail
service.

On 5/3/2022 9:59 AM, Ben wrote:
> olcott <polcott2@gmail.com> writes:
>
>> On 5/2/2022 9:21 PM, Ben wrote:
>>> olcott <polcott2@gmail.com> writes:
>>>
>>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>
>>>>>> Thanks for confirmation, that's what exactly what I was trying to tell
>>>>>> to topic poster in one of my previous posts. Prolog in it's bare form
>>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>>
>>>>>> If you want to deal with such problems maybe it is better to use Coq
>>>>>> theorem prover, I've never used it by myself, but it looks like one of
>>>>>> the best proving assistants out there.
>>>>>
>>>>> And indeed there is a fully formalised proof of GIT in Coq (though I
>>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>
>>>> It is true that G is not provable.
>>> G is provable. Proofs abound. I was pointing out one in a proper proof
>>> assistant, Coq.
>>
>> It is OK that you are not a math guy.
>
> You are not a math guy. I am.
>
>> If you were a math guy you would understand that if G is provable then
>> that makes Gödel totally wrong. G is not Gödel's theorem, it is a key
>> element of his theorem.
>
> No. G is provable. Though I did make a mistake -- the link was to a
> proof of G-RIT not G.
>

Then you would know that this is the mathematical definition of
Incompleteness: Incomplete(PA) ↔ ∃G ((PA ⊬ G) ∧ (PA ⊬ ¬G)).

Incomplete PA means that there exists a G such that G is not provable or
refutable in formal system PA.

Since you don't know this that proves you are not a math guy relative to
Gödel's 1931 Incompleteness Theorem.

> How are you getting on with E and specifying P? Have you given up?
>

I decided to write the whole TM interpreter from scratch. It will have
this file format:
Quintuples of ASCII text with inline comments
BEGIN_TAPE // on a line by itself.
Initial Tape Data // lines of ASCII text delimited by newline.

It will output a complete execution trace.
When I have the design of this system as my basis:
http://www.lns.mit.edu/~dsw/turing/turing.html

Writing a TM interpreter from scratch is nearly trivial.

My TM interpreter will start out with the same kind of 7-bit states and
characters that the above system has. This is trivially expanded to
8-bit, 16-bit or 32-bit hexadecimal.

The system currently reads lines of text from a text file.
I have to change this to reads lines of text from a specified input
parameter filename.

I may be able to write the whole system within four labor hours after
that. I forget how to read lines of text, so that took a while.

I can publish the source code when I am done. I will probably call it
"Simplest TM interpreter." I may publish it on GIT hub, I already have
an account.

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

On 5/3/2022 10:18 AM, André G. Isaak wrote:
> On 2022-05-02 18:57, olcott wrote:
>> On 5/2/2022 6:43 PM, Ben wrote:
>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>
>>>>> IF you are defining that your logic system is limited to what
>>>>> Prolog can "Prove", that is fine. Just realize that you have just
>>>>> defined that your
>>>>> logic system can't handle a lot of the real problems in the world,
>>>>> and in particular, it is very limited in the mathematics it can
>>>>> handle.
>>>>> I am pretty sure that Prolog is NOT up to handling the logic needed to
>>>>> handle the mathematics needed to express Godel's G, or the Halting
>>>>> Problem.
>>>>> Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
>>>>> have only proven that your limited logic system can't reach them in
>>>>> expressibility.
>>>>
>>>> Thanks for confirmation, that's what exactly what I was trying to tell
>>>> to topic poster in one of my previous posts. Prolog in it's bare form
>>>> is a bad theorem solver. It wasn't designed a such.
>>>>
>>>> If you want to deal with such problems maybe it is better to use Coq
>>>> theorem prover, I've never used it by myself, but it looks like one of
>>>> the best proving assistants out there.
>>>
>>> And indeed there is a fully formalised proof of GIT in Coq (though I
>>> think it's the slightly tighter Gödel-Rosser version).
>>>
>>
>> It is true that G is not provable. G is not provable because it is
>> semantically incorrect in the exactly same way that the Liar Paradox
>> is semantically incorrect.
>>
>> Gödel says:
>> 14 Every epistemological antinomy can likewise be used for a similar
>> undecidability proof
>>
>> André denied this six times yesterday
>> The Liar Paradox is an epistemological antinomy, thus can likewise be
>> used for a similar undecidability proof.
>
> No.
> The Liar can be used to construct an *identical* proof.

Really?

> Other
> antinomies could be used for similar proofs. He's already talking about
> The Liar.
>
>> Which means that the Liar Paradox is sufficiently equivalent to
>> Gödel's G. Which means if the basic mechanism of epistemological
>> antinomy is shown to be semantically incorrect then Gödel's G is shown
>> to be semantically incorrect.
>
> You have some serious reading comprehension problems. I never denied the
> things Gödel wrote. I denied your conclusion because it does not follow.
>
> Gödel starts by claiming there is a close relationship (*not*
> equivalence) between one particular antinomy, The Liar, and his G.
>
> He then states that similar proofs could be constructed using any antinomy.
>
> That entails that other antinomies could be used to construct similar
> proofs involving a similar close relation (again, *not* equivalence).
>

That you persisted (six times) on claiming that Gödel's statement about
the Liar Paradox overrode and superseded his statement about the entire
category that the Liar Paradox belongs to was despicably deceitful,
unless you believe that "close relationship" is stronger than "similar
undecidability proof". In that case you never lied about this. I really
only want an honest dialogue so I am happy to admit my mistakes.

> Gödel never claims *any* antinomy is equivalent to his G. Merely that a
> close relationship holds.
>

I take "similar undecidability proof" to mean isomorphic.
https://en.wikipedia.org/wiki/Isomorphism
Without carefully studying the philosophical underpinnings of the
concept if incompleteness:

Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).

Incomplete T means that there exists a φ such that φ is not provable or
refutable in formal system T.

The above is the precise measure of isomorphism. Anything meeting the
above specification is isomorphic to Gödel's G.

One might not feel comfortable that isomorphic is what Gödel by "similar
undecidability proof". When we examine the above definition of
Incompleteness applied to the entire set of epistemological antinomies,
then we realize that all of them are making the category mistake (thanks
Flibble) of presuming that φ is a logic sentence / truth bearer.

Here is my first example of a category / type mismatch error that I
wrote back in 2004: "What time is it (yes or no)?"

> And all my comments con
cerned exactly what that relationship is.
>
> André
>

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

On 2022-05-03 10:08, olcott wrote:
> On 5/3/2022 10:18 AM, André G. Isaak wrote:
>> On 2022-05-02 18:57, olcott wrote:
>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>>
>>>>>> IF you are defining that your logic system is limited to what
>>>>>> Prolog can "Prove", that is fine. Just realize that you have just
>>>>>> defined that your
>>>>>> logic system can't handle a lot of the real problems in the world,
>>>>>> and in particular, it is very limited in the mathematics it can
>>>>>> handle.
>>>>>> I am pretty sure that Prolog is NOT up to handling the logic
>>>>>> needed to
>>>>>> handle the mathematics needed to express Godel's G, or the Halting
>>>>>> Problem.
>>>>>> Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
>>>>>> have only proven that your limited logic system can't reach them
>>>>>> in expressibility.
>>>>>
>>>>> Thanks for confirmation, that's what exactly what I was trying to tell
>>>>> to topic poster in one of my previous posts. Prolog in it's bare form
>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>
>>>>> If you want to deal with such problems maybe it is better to use Coq
>>>>> theorem prover, I've never used it by myself, but it looks like one of
>>>>> the best proving assistants out there.
>>>>
>>>> And indeed there is a fully formalised proof of GIT in Coq (though I
>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>
>>>
>>> It is true that G is not provable. G is not provable because it is
>>> semantically incorrect in the exactly same way that the Liar Paradox
>>> is semantically incorrect.
>>>
>>> Gödel says:
>>> 14 Every epistemological antinomy can likewise be used for a similar
>>> undecidability proof
>>>
>>> André denied this six times yesterday
>>> The Liar Paradox is an epistemological antinomy, thus can likewise be
>>> used for a similar undecidability proof.
>>
>> No. The Liar can be used to construct an *identical* proof.
>
> Really?

Of course really.

His original proof drew on The Liar for inspiration. So a proof which
draws on The Liar would be the same proof.

He is saying that he could have used ANY antinomy.

IOW, he could have chosen a *different* antinomy from The Liar, call it
Antinomy X, and constructed a *similar* proof around that. It would not
be the same proof, but it would involve constructing some sentence
G-Prime which held the same relation to Antinomy X as G hold to The Liar.

But there would not be an equivalence between G-Prime and X anymore than
there is an equivalence between G and The Liar.

This is the point I keep trying to drive home. There is NO EQUIVALENCE
between G and the The Liar. Only a close relationship.

>> Other antinomies could be used for similar proofs. He's already
>> talking about The Liar.
>>
>>> Which means that the Liar Paradox is sufficiently equivalent to
>>> Gödel's G. Which means if the basic mechanism of epistemological
>>> antinomy is shown to be semantically incorrect then Gödel's G is
>>> shown to be semantically incorrect.
>>
>> You have some serious reading comprehension problems. I never denied
>> the things Gödel wrote. I denied your conclusion because it does not
>> follow.
>>
>> Gödel starts by claiming there is a close relationship (*not*
>> equivalence) between one particular antinomy, The Liar, and his G.
>>
>> He then states that similar proofs could be constructed using any
>> antinomy.
>>
>> That entails that other antinomies could be used to construct similar
>> proofs involving a similar close relation (again, *not* equivalence).
>>
>
> That you persisted (six times) on claiming that Gödel's statement about
> the Liar Paradox overrode and superseded his statement about the entire
> category that the Liar Paradox belongs to was despicably deceitful,

Except I made no such claim. Not even once. You persisted (six times) in
misreading my claim.

> unless you believe that "close relationship" is stronger than "similar
> undecidability proof". In that case you never lied about this. I really
> only want an honest dialogue so I am happy to admit my mistakes.
>
>> Gödel never claims *any* antinomy is equivalent to his G. Merely that
>> a close relationship holds.
>>
>
> I take "similar undecidability proof" to mean isomorphic.

Fine. That would mean the proof involving the Liar and G would be
isomorphic to the proof involving antinomy X and G-Prime.

That does *NOT* get you to the claim you were making which was that G in
some sense equivalent to The Liar. It is not.

And your claim that G is not a truth bearer rests on your false claim
that G and The Liar are somehow equivalent (though you refuse to say
with respect to what). G is very clearly a truth-bearer. Go back and
reread my original explanation.

> https://en.wikipedia.org/wiki/Isomorphism
> Without carefully studying the philosophical underpinnings of the
> concept if incompleteness:
>
> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>
> Incomplete T means that there exists a φ such that φ is not provable or
> refutable in formal system T.
>
> The above is the precise measure of isomorphism. Anything meeting the
> above specification is isomorphic to Gödel's G.
>
> One might not feel comfortable that isomorphic is what Gödel by "similar
> undecidability proof". When we examine the above definition of
> Incompleteness applied to the entire set of epistemological antinomies,
> then we realize that all of them are making the category mistake (thanks
> Flibble) of presuming that φ is a logic sentence / truth bearer.

Gödel's G is most definitely a truth bearer. It asserts that a specific
polynomial equation has an integer solution. That claim must either be
true or false.

André

--
To email remove 'invalid' & replace 'gm' with well known Google mail
service.

On 5/3/2022 11:52 AM, André G. Isaak wrote:
> On 2022-05-03 10:08, olcott wrote:
>> On 5/3/2022 10:18 AM, André G. Isaak wrote:
>>> On 2022-05-02 18:57, olcott wrote:
>>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>>>
>>>>>>> IF you are defining that your logic system is limited to what
>>>>>>> Prolog can "Prove", that is fine. Just realize that you have just
>>>>>>> defined that your
>>>>>>> logic system can't handle a lot of the real problems in the
>>>>>>> world, and in particular, it is very limited in the mathematics
>>>>>>> it can handle.
>>>>>>> I am pretty sure that Prolog is NOT up to handling the logic
>>>>>>> needed to
>>>>>>> handle the mathematics needed to express Godel's G, or the
>>>>>>> Halting Problem.
>>>>>>> Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
>>>>>>> have only proven that your limited logic system can't reach them
>>>>>>> in expressibility.
>>>>>>
>>>>>> Thanks for confirmation, that's what exactly what I was trying to
>>>>>> tell
>>>>>> to topic poster in one of my previous posts. Prolog in it's bare form
>>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>>
>>>>>> If you want to deal with such problems maybe it is better to use Coq
>>>>>> theorem prover, I've never used it by myself, but it looks like
>>>>>> one of
>>>>>> the best proving assistants out there.
>>>>>
>>>>> And indeed there is a fully formalised proof of GIT in Coq (though I
>>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>>
>>>>
>>>> It is true that G is not provable. G is not provable because it is
>>>> semantically incorrect in the exactly same way that the Liar Paradox
>>>> is semantically incorrect.
>>>>
>>>> Gödel says:
>>>> 14 Every epistemological antinomy can likewise be used for a similar
>>>> undecidability proof
>>>>
>>>> André denied this six times yesterday
>>>> The Liar Paradox is an epistemological antinomy, thus can likewise
>>>> be used for a similar undecidability proof.
>>>
>>> No. The Liar can be used to construct an *identical* proof.
>>
>> Really?
>
> Of course really.
>
> His original proof drew on The Liar for inspiration. So a proof which
> draws on The Liar would be the same proof.
>
> He is saying that he could have used ANY antinomy.
>
> IOW, he could have chosen a *different* antinomy from The Liar, call it
> Antinomy X, and constructed a *similar* proof around that. It would not
> be the same proof, but it would involve constructing some sentence
> G-Prime which held the same relation to Antinomy X as G hold to The Liar.
>
> But there would not be an equivalence between G-Prime and X anymore than
> there is an equivalence between G and The Liar.
>
> This is the point I keep trying to drive home. There is NO EQUIVALENCE
> between G and the The Liar. Only a close relationship.
>
>>> Other antinomies could be used for similar proofs. He's already
>>> talking about The Liar.
>>>
>>>> Which means that the Liar Paradox is sufficiently equivalent to
>>>> Gödel's G. Which means if the basic mechanism of epistemological
>>>> antinomy is shown to be semantically incorrect then Gödel's G is
>>>> shown to be semantically incorrect.
>>>
>>> You have some serious reading comprehension problems. I never denied
>>> the things Gödel wrote. I denied your conclusion because it does not
>>> follow.
>>>
>>> Gödel starts by claiming there is a close relationship (*not*
>>> equivalence) between one particular antinomy, The Liar, and his G.
>>>
>>> He then states that similar proofs could be constructed using any
>>> antinomy.
>>>
>>> That entails that other antinomies could be used to construct similar
>>> proofs involving a similar close relation (again, *not* equivalence).
>>>
>>
>> That you persisted (six times) on claiming that Gödel's statement
>> about the Liar Paradox overrode and superseded his statement about the
>> entire category that the Liar Paradox belongs to was despicably
>> deceitful,
>
> Except I made no such claim. Not even once. You persisted (six times) in
> misreading my claim.
>
>> unless you believe that "close relationship" is stronger than "similar
>> undecidability proof". In that case you never lied about this. I
>> really only want an honest dialogue so I am happy to admit my mistakes.
>>
>>> Gödel never claims *any* antinomy is equivalent to his G. Merely that
>>> a close relationship holds.
>>>
>>
>> I take "similar undecidability proof" to mean isomorphic.
>
> Fine. That would mean the proof involving the Liar and G would be
> isomorphic to the proof involving antinomy X and G-Prime.
>

I have no idea what you mean by G-Prime.

> That does *NOT* get you to the claim you were making which was that G in
> some sense equivalent to The Liar. It is not.
>
> And your claim that G is not a truth bearer rests on your false claim
> that G and The Liar are somehow equivalent (though you refuse to say
> with respect to what).

Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
It is the fact that the mathematical definition of Incompleteness simply
assumes that φ is semantically correct that is the core mistake of the
mathematical definition of Incompleteness.

> G is very clearly a truth-bearer. Go back and
> reread my original explanation.
>

When G is not provable in PA, how is it shown to be true?
If it is not shown to be true in PA then we have the strawman error.

>> https://en.wikipedia.org/wiki/Isomorphism
>> Without carefully studying the philosophical underpinnings of the
>> concept if incompleteness:
>>
>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>
>> Incomplete T means that there exists a φ such that φ is not provable
>> or refutable in formal system T.
>>
>> The above is the precise measure of isomorphism. Anything meeting the
>> above specification is isomorphic to Gödel's G.
>>
>> One might not feel comfortable that isomorphic is what Gödel by
>> "similar undecidability proof". When we examine the above definition
>> of Incompleteness applied to the entire set of epistemological
>> antinomies, then we realize that all of them are making the category
>> mistake (thanks Flibble) of presuming that φ is a logic sentence /
>> truth bearer.
>
> Gödel's G is most definitely a truth bearer. It asserts that a specific
> polynomial equation has an integer solution. That claim must either be
> true or false.
>
> André
>

When G is not provable in PA, how is it shown to be true?
If it is not shown to be true in PA then we have the strawman error.

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

On 5/3/2022 11:52 AM, André G. Isaak wrote:
> On 2022-05-03 10:08, olcott wrote:
>> On 5/3/2022 10:18 AM, André G. Isaak wrote:
>>> On 2022-05-02 18:57, olcott wrote:
>>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>>>
>>>>>>> IF you are defining that your logic system is limited to what
>>>>>>> Prolog can "Prove", that is fine. Just realize that you have just
>>>>>>> defined that your
>>>>>>> logic system can't handle a lot of the real problems in the
>>>>>>> world, and in particular, it is very limited in the mathematics
>>>>>>> it can handle.
>>>>>>> I am pretty sure that Prolog is NOT up to handling the logic
>>>>>>> needed to
>>>>>>> handle the mathematics needed to express Godel's G, or the
>>>>>>> Halting Problem.
>>>>>>> Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
>>>>>>> have only proven that your limited logic system can't reach them
>>>>>>> in expressibility.
>>>>>>
>>>>>> Thanks for confirmation, that's what exactly what I was trying to
>>>>>> tell
>>>>>> to topic poster in one of my previous posts. Prolog in it's bare form
>>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>>
>>>>>> If you want to deal with such problems maybe it is better to use Coq
>>>>>> theorem prover, I've never used it by myself, but it looks like
>>>>>> one of
>>>>>> the best proving assistants out there.
>>>>>
>>>>> And indeed there is a fully formalised proof of GIT in Coq (though I
>>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>>
>>>>
>>>> It is true that G is not provable. G is not provable because it is
>>>> semantically incorrect in the exactly same way that the Liar Paradox
>>>> is semantically incorrect.
>>>>
>>>> Gödel says:
>>>> 14 Every epistemological antinomy can likewise be used for a similar
>>>> undecidability proof
>>>>
>>>> André denied this six times yesterday
>>>> The Liar Paradox is an epistemological antinomy, thus can likewise
>>>> be used for a similar undecidability proof.
>>>
>>> No. The Liar can be used to construct an *identical* proof.
>>
>> Really?
>
> Of course really.
>
> His original proof drew on The Liar for inspiration. So a proof which
> draws on The Liar would be the same proof.

OK, then I am very happy to say that my accusation that you lied was not
justified, we were simply talking past each other.

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

On Tuesday, May 3, 2022 at 1:08:50 PM UTC-4, olcott wrote:
> On 5/3/2022 11:52 AM, André G. Isaak wrote:
> > On 2022-05-03 10:08, olcott wrote:
> >> On 5/3/2022 10:18 AM, André G. Isaak wrote:
> >>> On 2022-05-02 18:57, olcott wrote:
> >>>> On 5/2/2022 6:43 PM, Ben wrote:
> >>>>> Aleksy Grabowski <hur...@gmail.com> writes:
> >>>>>
> >>>>>>> IF you are defining that your logic system is limited to what
> >>>>>>> Prolog can "Prove", that is fine. Just realize that you have just
> >>>>>>> defined that your
> >>>>>>> logic system can't handle a lot of the real problems in the
> >>>>>>> world, and in particular, it is very limited in the mathematics
> >>>>>>> it can handle.
> >>>>>>> I am pretty sure that Prolog is NOT up to handling the logic
> >>>>>>> needed to
> >>>>>>> handle the mathematics needed to express Godel's G, or the
> >>>>>>> Halting Problem.
> >>>>>>> Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
> >>>>>>> have only proven that your limited logic system can't reach them
> >>>>>>> in expressibility.
> >>>>>>
> >>>>>> Thanks for confirmation, that's what exactly what I was trying to
> >>>>>> tell
> >>>>>> to topic poster in one of my previous posts. Prolog in it's bare form
> >>>>>> is a bad theorem solver. It wasn't designed a such.
> >>>>>>
> >>>>>> If you want to deal with such problems maybe it is better to use Coq
> >>>>>> theorem prover, I've never used it by myself, but it looks like
> >>>>>> one of
> >>>>>> the best proving assistants out there.
> >>>>>
> >>>>> And indeed there is a fully formalised proof of GIT in Coq (though I
> >>>>> think it's the slightly tighter Gödel-Rosser version).
> >>>>>
> >>>>
> >>>> It is true that G is not provable. G is not provable because it is
> >>>> semantically incorrect in the exactly same way that the Liar Paradox
> >>>> is semantically incorrect.
> >>>>
> >>>> Gödel says:
> >>>> 14 Every epistemological antinomy can likewise be used for a similar
> >>>> undecidability proof
> >>>>
> >>>> André denied this six times yesterday
> >>>> The Liar Paradox is an epistemological antinomy, thus can likewise
> >>>> be used for a similar undecidability proof.
> >>>
> >>> No. The Liar can be used to construct an *identical* proof.
> >>
> >> Really?
> >
> > Of course really.
> >
> > His original proof drew on The Liar for inspiration. So a proof which
> > draws on The Liar would be the same proof.
> OK, then I am very happy to say that my accusation that you lied was not
> justified, we were simply talking past each other.
> --
> Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
> Genius hits a target no one else can see." Arthur Schopenhauer

I hope you don't mind my interrupting, but are you using the WTD code to say something? If you don't answer I'll assume you mean "no" and aren't saying anything to interfere with me in code, and that your messages are intended to be interpreted in that way, as code-free.

-Philip White

On 2022-05-03 11:05, olcott wrote:
> On 5/3/2022 11:52 AM, André G. Isaak wrote:
>> On 2022-05-03 10:08, olcott wrote:
>>> On 5/3/2022 10:18 AM, André G. Isaak wrote:
>>>> On 2022-05-02 18:57, olcott wrote:
>>>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>>>>
>>>>>>>> IF you are defining that your logic system is limited to what
>>>>>>>> Prolog can "Prove", that is fine. Just realize that you have
>>>>>>>> just defined that your
>>>>>>>> logic system can't handle a lot of the real problems in the
>>>>>>>> world, and in particular, it is very limited in the mathematics
>>>>>>>> it can handle.
>>>>>>>> I am pretty sure that Prolog is NOT up to handling the logic
>>>>>>>> needed to
>>>>>>>> handle the mathematics needed to express Godel's G, or the
>>>>>>>> Halting Problem.
>>>>>>>> Thus, your "Proof" that these Theorems are "Wrong" is incorrect,
>>>>>>>> you
>>>>>>>> have only proven that your limited logic system can't reach them
>>>>>>>> in expressibility.
>>>>>>>
>>>>>>> Thanks for confirmation, that's what exactly what I was trying to
>>>>>>> tell
>>>>>>> to topic poster in one of my previous posts. Prolog in it's bare
>>>>>>> form
>>>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>>>
>>>>>>> If you want to deal with such problems maybe it is better to use Coq
>>>>>>> theorem prover, I've never used it by myself, but it looks like
>>>>>>> one of
>>>>>>> the best proving assistants out there.
>>>>>>
>>>>>> And indeed there is a fully formalised proof of GIT in Coq (though I
>>>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>>>
>>>>>
>>>>> It is true that G is not provable. G is not provable because it is
>>>>> semantically incorrect in the exactly same way that the Liar
>>>>> Paradox is semantically incorrect.
>>>>>
>>>>> Gödel says:
>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>> similar undecidability proof
>>>>>
>>>>> André denied this six times yesterday
>>>>> The Liar Paradox is an epistemological antinomy, thus can likewise
>>>>> be used for a similar undecidability proof.
>>>>
>>>> No. The Liar can be used to construct an *identical* proof.
>>>
>>> Really?
>>
>> Of course really.
>>
>> His original proof drew on The Liar for inspiration. So a proof which
>> draws on The Liar would be the same proof.
>>
>> He is saying that he could have used ANY antinomy.
>>
>> IOW, he could have chosen a *different* antinomy from The Liar, call
>> it Antinomy X, and constructed a *similar* proof around that. It would
>> not be the same proof, but it would involve constructing some sentence
>> G-Prime which held the same relation to Antinomy X as G hold to The Liar.
>>
>> But there would not be an equivalence between G-Prime and X anymore
>> than there is an equivalence between G and The Liar.
>>
>> This is the point I keep trying to drive home. There is NO EQUIVALENCE
>> between G and the The Liar. Only a close relationship.
>>
>>>> Other antinomies could be used for similar proofs. He's already
>>>> talking about The Liar.
>>>>
>>>>> Which means that the Liar Paradox is sufficiently equivalent to
>>>>> Gödel's G. Which means if the basic mechanism of epistemological
>>>>> antinomy is shown to be semantically incorrect then Gödel's G is
>>>>> shown to be semantically incorrect.
>>>>
>>>> You have some serious reading comprehension problems. I never denied
>>>> the things Gödel wrote. I denied your conclusion because it does not
>>>> follow.
>>>>
>>>> Gödel starts by claiming there is a close relationship (*not*
>>>> equivalence) between one particular antinomy, The Liar, and his G.
>>>>
>>>> He then states that similar proofs could be constructed using any
>>>> antinomy.
>>>>
>>>> That entails that other antinomies could be used to construct
>>>> similar proofs involving a similar close relation (again, *not*
>>>> equivalence).
>>>>
>>>
>>> That you persisted (six times) on claiming that Gödel's statement
>>> about the Liar Paradox overrode and superseded his statement about
>>> the entire category that the Liar Paradox belongs to was despicably
>>> deceitful,
>>
>> Except I made no such claim. Not even once. You persisted (six times)
>> in misreading my claim.
>>
>>> unless you believe that "close relationship" is stronger than
>>> "similar undecidability proof". In that case you never lied about
>>> this. I really only want an honest dialogue so I am happy to admit my
>>> mistakes.
>>>
>>>> Gödel never claims *any* antinomy is equivalent to his G. Merely
>>>> that a close relationship holds.
>>>>
>>>
>>> I take "similar undecidability proof" to mean isomorphic.
>>
>> Fine. That would mean the proof involving the Liar and G would be
>> isomorphic to the proof involving antinomy X and G-Prime.
>>
>
> I have no idea what you mean by G-Prime.

It is defined directly above. Trying reading more carefully.

>> That does *NOT* get you to the claim you were making which was that G
>> in some sense equivalent to The Liar. It is not.
>>
>> And your claim that G is not a truth bearer rests on your false claim
>> that G and The Liar are somehow equivalent (though you refuse to say
>> with respect to what).
>
> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
> It is the fact that the mathematical definition of Incompleteness simply
> assumes that φ is semantically correct that is the core mistake of the
> mathematical definition of Incompleteness.
>
>> G is very clearly a truth-bearer. Go back and reread my original
>> explanation.
>>
>
> When G is not provable in PA, how is it shown to be true?
> If it is not shown to be true in PA then we have the strawman error.

Here you're simply begging the question by assuming your own conclusion:
that being true and being provable are the same. The whole point of
Gödel's proof is that they cannot be the same (at least not for
non-trivial systems).

The question is not whether it is true but whether it is a truth *bearer*.

You make the claim that The Liar is not a truth bearer (a plausible
claim depending on one's definitions).

You then jump to the conclusion that G is not a truth bearer based on
your assertion that it is "equivalent" to The Liar. But it is *NOT*
equivalent. It merely bears a close relationship. But you refuse to
actually consider what the nature of that relationship; there are both
similiarites and differences.

Whereas the Liar has no content other than to assert its own falsity,
Gödel's G has definite content. It does not assert its own
unprovability, it asserts a very specific mathematical claim, one which
must by its nature be either true or false. Therefore G *is* a truth bearer.

The formulation that G asserts its own unprovability is the Cliff-Notes
version of the proof. It's not the substance of the actual proof.

André

--
To email remove 'invalid' & replace 'gm' with well known Google mail
service.

On 5/3/2022 12:13 PM, B.H. wrote:
> On Tuesday, May 3, 2022 at 1:08:50 PM UTC-4, olcott wrote:
>> On 5/3/2022 11:52 AM, André G. Isaak wrote:
>>> On 2022-05-03 10:08, olcott wrote:
>>>> On 5/3/2022 10:18 AM, André G. Isaak wrote:
>>>>> On 2022-05-02 18:57, olcott wrote:
>>>>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>>>>> Aleksy Grabowski <hur...@gmail.com> writes:
>>>>>>>
>>>>>>>>> IF you are defining that your logic system is limited to what
>>>>>>>>> Prolog can "Prove", that is fine. Just realize that you have just
>>>>>>>>> defined that your
>>>>>>>>> logic system can't handle a lot of the real problems in the
>>>>>>>>> world, and in particular, it is very limited in the mathematics
>>>>>>>>> it can handle.
>>>>>>>>> I am pretty sure that Prolog is NOT up to handling the logic
>>>>>>>>> needed to
>>>>>>>>> handle the mathematics needed to express Godel's G, or the
>>>>>>>>> Halting Problem.
>>>>>>>>> Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
>>>>>>>>> have only proven that your limited logic system can't reach them
>>>>>>>>> in expressibility.
>>>>>>>>
>>>>>>>> Thanks for confirmation, that's what exactly what I was trying to
>>>>>>>> tell
>>>>>>>> to topic poster in one of my previous posts. Prolog in it's bare form
>>>>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>>>>
>>>>>>>> If you want to deal with such problems maybe it is better to use Coq
>>>>>>>> theorem prover, I've never used it by myself, but it looks like
>>>>>>>> one of
>>>>>>>> the best proving assistants out there.
>>>>>>>
>>>>>>> And indeed there is a fully formalised proof of GIT in Coq (though I
>>>>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>>>>
>>>>>>
>>>>>> It is true that G is not provable. G is not provable because it is
>>>>>> semantically incorrect in the exactly same way that the Liar Paradox
>>>>>> is semantically incorrect.
>>>>>>
>>>>>> Gödel says:
>>>>>> 14 Every epistemological antinomy can likewise be used for a similar
>>>>>> undecidability proof
>>>>>>
>>>>>> André denied this six times yesterday
>>>>>> The Liar Paradox is an epistemological antinomy, thus can likewise
>>>>>> be used for a similar undecidability proof.
>>>>>
>>>>> No. The Liar can be used to construct an *identical* proof.
>>>>
>>>> Really?
>>>
>>> Of course really.
>>>
>>> His original proof drew on The Liar for inspiration. So a proof which
>>> draws on The Liar would be the same proof.
>> OK, then I am very happy to say that my accusation that you lied was not
>> justified, we were simply talking past each other.
>> --
>> Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
>> Genius hits a target no one else can see." Arthur Schopenhauer
>
> I hope you don't mind my interrupting, but are you using the WTD code to say something?

I have no idea what you mean.
I am using C/x86 and symbolic logic to formalize what I am saying.

> If you don't answer I'll assume you mean "no" and aren't saying anything to interfere with me in code, and that your messages are intended to be interpreted in that way, as code-free.
>
> -Philip White

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

On Tuesday, May 3, 2022 at 1:17:41 PM UTC-4, olcott wrote:
> On 5/3/2022 12:13 PM, B.H. wrote:
> > On Tuesday, May 3, 2022 at 1:08:50 PM UTC-4, olcott wrote:
> >> On 5/3/2022 11:52 AM, André G. Isaak wrote:
> >>> On 2022-05-03 10:08, olcott wrote:
> >>>> On 5/3/2022 10:18 AM, André G. Isaak wrote:
> >>>>> On 2022-05-02 18:57, olcott wrote:
> >>>>>> On 5/2/2022 6:43 PM, Ben wrote:
> >>>>>>> Aleksy Grabowski <hur...@gmail.com> writes:
> >>>>>>>
> >>>>>>>>> IF you are defining that your logic system is limited to what
> >>>>>>>>> Prolog can "Prove", that is fine. Just realize that you have just
> >>>>>>>>> defined that your
> >>>>>>>>> logic system can't handle a lot of the real problems in the
> >>>>>>>>> world, and in particular, it is very limited in the mathematics
> >>>>>>>>> it can handle.
> >>>>>>>>> I am pretty sure that Prolog is NOT up to handling the logic
> >>>>>>>>> needed to
> >>>>>>>>> handle the mathematics needed to express Godel's G, or the
> >>>>>>>>> Halting Problem.
> >>>>>>>>> Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
> >>>>>>>>> have only proven that your limited logic system can't reach them
> >>>>>>>>> in expressibility.
> >>>>>>>>
> >>>>>>>> Thanks for confirmation, that's what exactly what I was trying to
> >>>>>>>> tell
> >>>>>>>> to topic poster in one of my previous posts. Prolog in it's bare form
> >>>>>>>> is a bad theorem solver. It wasn't designed a such.
> >>>>>>>>
> >>>>>>>> If you want to deal with such problems maybe it is better to use Coq
> >>>>>>>> theorem prover, I've never used it by myself, but it looks like
> >>>>>>>> one of
> >>>>>>>> the best proving assistants out there.
> >>>>>>>
> >>>>>>> And indeed there is a fully formalised proof of GIT in Coq (though I
> >>>>>>> think it's the slightly tighter Gödel-Rosser version).
> >>>>>>>
> >>>>>>
> >>>>>> It is true that G is not provable. G is not provable because it is
> >>>>>> semantically incorrect in the exactly same way that the Liar Paradox
> >>>>>> is semantically incorrect.
> >>>>>>
> >>>>>> Gödel says:
> >>>>>> 14 Every epistemological antinomy can likewise be used for a similar
> >>>>>> undecidability proof
> >>>>>>
> >>>>>> André denied this six times yesterday
> >>>>>> The Liar Paradox is an epistemological antinomy, thus can likewise
> >>>>>> be used for a similar undecidability proof.
> >>>>>
> >>>>> No. The Liar can be used to construct an *identical* proof.
> >>>>
> >>>> Really?
> >>>
> >>> Of course really.
> >>>
> >>> His original proof drew on The Liar for inspiration. So a proof which
> >>> draws on The Liar would be the same proof.
> >> OK, then I am very happy to say that my accusation that you lied was not
> >> justified, we were simply talking past each other.
> >> --
> >> Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
> >> Genius hits a target no one else can see." Arthur Schopenhauer
> >
> > I hope you don't mind my interrupting, but are you using the WTD code to say something?
> I have no idea what you mean.
> I am using C/x86 and symbolic logic to formalize what I am saying.
> > If you don't answer I'll assume you mean "no" and aren't saying anything to interfere with me in code, and that your messages are intended to be interpreted in that way, as code-free.
> >
> > -Philip White
> --
> Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
> Genius hits a target no one else can see." Arthur Schopenhauer

That is good, I almost never use that code either...I would tend to mention it if I were using it. I appreciate that you answered me.

-Philip

On 5/3/2022 12:17 PM, André G. Isaak wrote:
> On 2022-05-03 11:05, olcott wrote:
>> On 5/3/2022 11:52 AM, André G. Isaak wrote:
>>> On 2022-05-03 10:08, olcott wrote:
>>>> On 5/3/2022 10:18 AM, André G. Isaak wrote:
>>>>> On 2022-05-02 18:57, olcott wrote:
>>>>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>>>>>
>>>>>>>>> IF you are defining that your logic system is limited to what
>>>>>>>>> Prolog can "Prove", that is fine. Just realize that you have
>>>>>>>>> just defined that your
>>>>>>>>> logic system can't handle a lot of the real problems in the
>>>>>>>>> world, and in particular, it is very limited in the mathematics
>>>>>>>>> it can handle.
>>>>>>>>> I am pretty sure that Prolog is NOT up to handling the logic
>>>>>>>>> needed to
>>>>>>>>> handle the mathematics needed to express Godel's G, or the
>>>>>>>>> Halting Problem.
>>>>>>>>> Thus, your "Proof" that these Theorems are "Wrong" is
>>>>>>>>> incorrect, you
>>>>>>>>> have only proven that your limited logic system can't reach
>>>>>>>>> them in expressibility.
>>>>>>>>
>>>>>>>> Thanks for confirmation, that's what exactly what I was trying
>>>>>>>> to tell
>>>>>>>> to topic poster in one of my previous posts. Prolog in it's bare
>>>>>>>> form
>>>>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>>>>
>>>>>>>> If you want to deal with such problems maybe it is better to use
>>>>>>>> Coq
>>>>>>>> theorem prover, I've never used it by myself, but it looks like
>>>>>>>> one of
>>>>>>>> the best proving assistants out there.
>>>>>>>
>>>>>>> And indeed there is a fully formalised proof of GIT in Coq (though I
>>>>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>>>>
>>>>>>
>>>>>> It is true that G is not provable. G is not provable because it is
>>>>>> semantically incorrect in the exactly same way that the Liar
>>>>>> Paradox is semantically incorrect.
>>>>>>
>>>>>> Gödel says:
>>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>>> similar undecidability proof
>>>>>>
>>>>>> André denied this six times yesterday
>>>>>> The Liar Paradox is an epistemological antinomy, thus can likewise
>>>>>> be used for a similar undecidability proof.
>>>>>
>>>>> No. The Liar can be used to construct an *identical* proof.
>>>>
>>>> Really?
>>>
>>> Of course really.
>>>
>>> His original proof drew on The Liar for inspiration. So a proof which
>>> draws on The Liar would be the same proof.
>>>
>>> He is saying that he could have used ANY antinomy.
>>>
>>> IOW, he could have chosen a *different* antinomy from The Liar, call
>>> it Antinomy X, and constructed a *similar* proof around that. It
>>> would not be the same proof, but it would involve constructing some
>>> sentence G-Prime which held the same relation to Antinomy X as G hold
>>> to The Liar.
>>>
>>> But there would not be an equivalence between G-Prime and X anymore
>>> than there is an equivalence between G and The Liar.
>>>
>>> This is the point I keep trying to drive home. There is NO
>>> EQUIVALENCE between G and the The Liar. Only a close relationship.
>>>
>>>>> Other antinomies could be used for similar proofs. He's already
>>>>> talking about The Liar.
>>>>>
>>>>>> Which means that the Liar Paradox is sufficiently equivalent to
>>>>>> Gödel's G. Which means if the basic mechanism of epistemological
>>>>>> antinomy is shown to be semantically incorrect then Gödel's G is
>>>>>> shown to be semantically incorrect.
>>>>>
>>>>> You have some serious reading comprehension problems. I never
>>>>> denied the things Gödel wrote. I denied your conclusion because it
>>>>> does not follow.
>>>>>
>>>>> Gödel starts by claiming there is a close relationship (*not*
>>>>> equivalence) between one particular antinomy, The Liar, and his G.
>>>>>
>>>>> He then states that similar proofs could be constructed using any
>>>>> antinomy.
>>>>>
>>>>> That entails that other antinomies could be used to construct
>>>>> similar proofs involving a similar close relation (again, *not*
>>>>> equivalence).
>>>>>
>>>>
>>>> That you persisted (six times) on claiming that Gödel's statement
>>>> about the Liar Paradox overrode and superseded his statement about
>>>> the entire category that the Liar Paradox belongs to was despicably
>>>> deceitful,
>>>
>>> Except I made no such claim. Not even once. You persisted (six times)
>>> in misreading my claim.
>>>
>>>> unless you believe that "close relationship" is stronger than
>>>> "similar undecidability proof". In that case you never lied about
>>>> this. I really only want an honest dialogue so I am happy to admit
>>>> my mistakes.
>>>>
>>>>> Gödel never claims *any* antinomy is equivalent to his G. Merely
>>>>> that a close relationship holds.
>>>>>
>>>>
>>>> I take "similar undecidability proof" to mean isomorphic.
>>>
>>> Fine. That would mean the proof involving the Liar and G would be
>>> isomorphic to the proof involving antinomy X and G-Prime.
>>>
>>
>> I have no idea what you mean by G-Prime.
>
> It is defined directly above. Trying reading more carefully.

OK.

>
>>> That does *NOT* get you to the claim you were making which was that G
>>> in some sense equivalent to The Liar. It is not.
>>>
>>> And your claim that G is not a truth bearer rests on your false claim
>>> that G and The Liar are somehow equivalent (though you refuse to say
>>> with respect to what).
>>
>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>> It is the fact that the mathematical definition of Incompleteness
>> simply assumes that φ is semantically correct that is the core mistake
>> of the mathematical definition of Incompleteness.
>>
>>> G is very clearly a truth-bearer. Go back and reread my original
>>> explanation.
>>>
>>
>> When G is not provable in PA, how is it shown to be true?
>> If it is not shown to be true in PA then we have the strawman error.
>
> Here you're simply begging the question by assuming your own conclusion:
> that being true and being provable are the same.

This is not any mere assumption.

The only way that any analytic expressions of language are correctly
determined to be true is:
(a) They are defined to be true.
(b) They are derived from applying truth preserving operations to (a) or
(b). Prolog knows this on the basis of its facts and rules. Facts are
(a) and rules are (b). This is also known as sound deductive inference.

> The whole point of
> Gödel's proof is that they cannot be the same (at least not for
> non-trivial systems).
>

When G is not provable in PA, how is it shown to be true (wild guess)?
What is the precise basis for assessing that G is true? please provide
ALL the steps.

> The question is not whether it is true but whether it is a truth *bearer*.
>
> You make the claim that The Liar is not a truth bearer (a plausible
> claim depending on one's definitions).
>
> You then jump to the conclusion that G is not a truth bearer based on
> your assertion that it is "equivalent" to The Liar. But it is *NOT*
> equivalent. It merely bears a close relationship. But you refuse to
> actually consider what the nature of that relationship; there are both
> similiarites and differences.
>

On 5/3/2022 12:25 PM, B.H. wrote:
> On Tuesday, May 3, 2022 at 1:17:41 PM UTC-4, olcott wrote:
>> On 5/3/2022 12:13 PM, B.H. wrote:
>>> On Tuesday, May 3, 2022 at 1:08:50 PM UTC-4, olcott wrote:
>>>> On 5/3/2022 11:52 AM, André G. Isaak wrote:
>>>>> On 2022-05-03 10:08, olcott wrote:
>>>>>> On 5/3/2022 10:18 AM, André G. Isaak wrote:
>>>>>>> On 2022-05-02 18:57, olcott wrote:
>>>>>>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>>>>>>> Aleksy Grabowski <hur...@gmail.com> writes:
>>>>>>>>>
>>>>>>>>>>> IF you are defining that your logic system is limited to what
>>>>>>>>>>> Prolog can "Prove", that is fine. Just realize that you have just
>>>>>>>>>>> defined that your
>>>>>>>>>>> logic system can't handle a lot of the real problems in the
>>>>>>>>>>> world, and in particular, it is very limited in the mathematics
>>>>>>>>>>> it can handle.
>>>>>>>>>>> I am pretty sure that Prolog is NOT up to handling the logic
>>>>>>>>>>> needed to
>>>>>>>>>>> handle the mathematics needed to express Godel's G, or the
>>>>>>>>>>> Halting Problem.
>>>>>>>>>>> Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
>>>>>>>>>>> have only proven that your limited logic system can't reach them
>>>>>>>>>>> in expressibility.
>>>>>>>>>>
>>>>>>>>>> Thanks for confirmation, that's what exactly what I was trying to
>>>>>>>>>> tell
>>>>>>>>>> to topic poster in one of my previous posts. Prolog in it's bare form
>>>>>>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>>>>>>
>>>>>>>>>> If you want to deal with such problems maybe it is better to use Coq
>>>>>>>>>> theorem prover, I've never used it by myself, but it looks like
>>>>>>>>>> one of
>>>>>>>>>> the best proving assistants out there.
>>>>>>>>>
>>>>>>>>> And indeed there is a fully formalised proof of GIT in Coq (though I
>>>>>>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>>>>>>
>>>>>>>>
>>>>>>>> It is true that G is not provable. G is not provable because it is
>>>>>>>> semantically incorrect in the exactly same way that the Liar Paradox
>>>>>>>> is semantically incorrect.
>>>>>>>>
>>>>>>>> Gödel says:
>>>>>>>> 14 Every epistemological antinomy can likewise be used for a similar
>>>>>>>> undecidability proof
>>>>>>>>
>>>>>>>> André denied this six times yesterday
>>>>>>>> The Liar Paradox is an epistemological antinomy, thus can likewise
>>>>>>>> be used for a similar undecidability proof.
>>>>>>>
>>>>>>> No. The Liar can be used to construct an *identical* proof.
>>>>>>
>>>>>> Really?
>>>>>
>>>>> Of course really.
>>>>>
>>>>> His original proof drew on The Liar for inspiration. So a proof which
>>>>> draws on The Liar would be the same proof.
>>>> OK, then I am very happy to say that my accusation that you lied was not
>>>> justified, we were simply talking past each other.
>>>> --
>>>> Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
>>>> Genius hits a target no one else can see." Arthur Schopenhauer
>>>
>>> I hope you don't mind my interrupting, but are you using the WTD code to say something?
>> I have no idea what you mean.
>> I am using C/x86 and symbolic logic to formalize what I am saying.
>>> If you don't answer I'll assume you mean "no" and aren't saying anything to interfere with me in code, and that your messages are intended to be interpreted in that way, as code-free.
>>>
>>> -Philip White
>> --
>> Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
>> Genius hits a target no one else can see." Arthur Schopenhauer
>
> That is good, I almost never use that code either...I would tend to mention it if I were using it. I appreciate that you answered me.
>
> -Philip

Sure. It seems that our dialogues are good and reasonable.

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

On 2022-05-03 11:33, olcott wrote:
> On 5/3/2022 12:17 PM, André G. Isaak wrote:
>> On 2022-05-03 11:05, olcott wrote:
>>> On 5/3/2022 11:52 AM, André G. Isaak wrote:

<snippage>

>>>> G is very clearly a truth-bearer. Go back and reread my original
>>>> explanation.
>>>>
>>>
>>> When G is not provable in PA, how is it shown to be true?
>>> If it is not shown to be true in PA then we have the strawman error.
>>
>> Here you're simply begging the question by assuming your own
>> conclusion: that being true and being provable are the same.
>
> This is not any mere assumption.
>
> The only way that any analytic expressions of language are correctly
> determined to be true is:

'True' and 'Correctly determined to be true' mean different things.

> (a) They are defined to be true.
> (b) They are derived from applying truth preserving operations to (a) or
> (b). Prolog knows this on the basis of its facts and rules. Facts are
> (a) and rules are (b). This is also known as sound deductive inference.

These are YOUR assumptions. They have not been demonstrated. And they
are not consistent with the way in which the rest of the world talks
about truth. You are talking about provability, not truth.

>> The whole point of Gödel's proof is that they cannot be the same (at
>> least not for non-trivial systems).
>>
>
> When G is not provable in PA, how is it shown to be true (wild guess)?
> What is the precise basis for assessing that G is true? please provide
> ALL the steps.

"True" and "Known to be true" are entirely different things.

Consider the equation Srt((2748 + 87)^3) = 150,948.776 (to 3 decimal places)

That equation is true but it is unlikely anyone knew this to be true
until now since I very much doubt anyone had previously considered that
specific equation. That's doesn't mean it wasn't true all along. Just
that no one knew it was true.

There are all sorts of cases where we know one thing without knowing all
things. I can know with certainty that (A ∨ B) is true meaning that I
know that *at least* one of A or B must be true while still not knowing
the truth value of either. These sorts of things occur all the time.

And not being provable in PA and not being provable are also two
different things.

>> The question is not whether it is true but whether it is a truth
>> *bearer*.
>>
>> You make the claim that The Liar is not a truth bearer (a plausible
>> claim depending on one's definitions).
>>
>> You then jump to the conclusion that G is not a truth bearer based on
>> your assertion that it is "equivalent" to The Liar. But it is *NOT*
>> equivalent. It merely bears a close relationship. But you refuse to
>> actually consider what the nature of that relationship; there are both
>> similiarites and differences.
>>
>
> Precise equivalence is defined by this:
> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>
> The Liar Paradox can be neither proven nor refuted where T is the entire
> body of analytic knowledge and φ is LP.

The Liar Paradox is a self-contradiction. The Gödel sentence is not.

>> Whereas the Liar has no content other than to assert its own falsity,
>> Gödel's G has definite content. It does not assert its own
>> unprovability, it asserts a very specific mathematical claim, one
>> which must by its nature be either true or false. Therefore G *is* a
>> truth bearer.
>>
>> The formulation that G asserts its own unprovability is the
>> Cliff-Notes version of the proof. It's not the substance of the actual
>> proof.
>>
>> André
>
> It is isomorphic to the substance of the actual proof.

No. It is not. G asserts a claim about mathematics. It does not assert
anything about itself. However, within the metalanguage we can prove
that G can only be true if it is not provable within the system under
consideration.

> Gödel says:
> since the undecidable proposition [R(q); q] states precisely that q
> belongs to K, i.e. according to (1), that [R(q); q] is not provable. We
> are therefore confronted with a proposition which asserts its own
> unprovability.

We are confronted *in our analysis* with such a situation. But there is
no proposition which directly asserts such a thing.

The problem is you refuse to look at the actual math and instead look
only at the text commentary which is merely a guide to, not the actual
substance of, the proof.

André

--
To email remove 'invalid' & replace 'gm' with well known Google mail
service.

On 5/3/2022 9:18 AM, André G. Isaak wrote:
> On 2022-05-02 18:57, olcott wrote:
IDIOT SNIPPED

> No. The Liar can be used to construct an *identical* proof. Other
> antinomies could be used for similar proofs. He's already talking about
> The Liar.
>
>> Which means that the Liar Paradox is sufficiently equivalent to
>> Gödel's G. Which means if the basic mechanism of epistemological
>> antinomy is shown to be semantically incorrect then Gödel's G is shown
>> to be semantically incorrect.
>
> You have some serious reading comprehension problems. I never denied the
> things Gödel wrote. I denied your conclusion because it does not follow.
>
> Gödel starts by claiming there is a close relationship (*not*
> equivalence) between one particular antinomy, The Liar, and his G.
>
> He then states that similar proofs could be constructed using any antinomy.
>
> That entails that other antinomies could be used to construct similar
> proofs involving a similar close relation (again, *not* equivalence).
>
> Gödel never claims *any* antinomy is equivalent to his G. Merely that a
> close relationship holds.
>
> And all my comments concerned exactly what that relationship is.
I think that you have provided the troll a similar explanation over 100
times. I admire your tenacity but I must ask you a question: Why do you
think one more time will do either him or you any good? It's not like
this is an educational or soul-improving opportunity for either of you;
for you this must be frustrating no matter your intentions and for him
he is what he is and this is his only amusement. Whether troll or
buffoon, he's proud of his appearance as wasted space.
--
Jeff Barnett

On 5/3/2022 1:23 PM, André G. Isaak wrote:
> On 2022-05-03 11:33, olcott wrote:
>> On 5/3/2022 12:17 PM, André G. Isaak wrote:
>>> On 2022-05-03 11:05, olcott wrote:
>>>> On 5/3/2022 11:52 AM, André G. Isaak wrote:
>
> <snippage>
>
>>>>> G is very clearly a truth-bearer. Go back and reread my original
>>>>> explanation.
>>>>>
>>>>
>>>> When G is not provable in PA, how is it shown to be true?
>>>> If it is not shown to be true in PA then we have the strawman error.
>>>
>>> Here you're simply begging the question by assuming your own
>>> conclusion: that being true and being provable are the same.
>>
>> This is not any mere assumption.
>>
>> The only way that any analytic expressions of language are correctly
>> determined to be true is:
>
> 'True' and 'Correctly determined to be true' mean different things.
>

Yes that seems to be correct.
On the other hand calling an expression of language true that has not be
'Correctly determined to be true' is an error.

If G is claimed to be true then this assertion must be supported by:
'Correctly determined to be true' otherwise the assessment of its truth
is no more than a wild guess.

>> (a) They are defined to be true.
>> (b) They are derived from applying truth preserving operations to (a)
>> or (b). Prolog knows this on the basis of its facts and rules. Facts
>> are (a) and rules are (b). This is also known as sound deductive
>> inference.
>
> These are YOUR assumptions. They have not been demonstrated. And they
> are not consistent with the way in which the rest of the world talks
> about truth. You are talking about provability, not truth.
>

If G is claimed to be true then this assertion must be supported by:
'Correctly determined to be true' otherwise the assessment of its truth
is no more than a wild guess.

>>> The whole point of Gödel's proof is that they cannot be the same (at
>>> least not for non-trivial systems).
>>>
>>
>> When G is not provable in PA, how is it shown to be true (wild guess)?
>> What is the precise basis for assessing that G is true? please provide
>> ALL the steps.
>
> "True" and "Known to be true" are entirely different things.
>

Yes, however:
If G is claimed to be true then this assertion must be supported by:
'Correctly determined to be true' otherwise the assessment of its truth
is no more than a wild guess.

> Consider the equation Srt((2748 + 87)^3) = 150,948.776 (to 3 decimal
> places)
>

(2748 + 87)^3 = 22,785,532,875
What are you sorting with Srt()?

> That equation is true but it is unlikely anyone knew this to be true
> until now since I very much doubt anyone had previously considered that
> specific equation. That's doesn't mean it wasn't true all along. Just
> that no one knew it was true.
>
> There are all sorts of cases where we know one thing without knowing all
> things. I can know with certainty that (A ∨ B) is true meaning that I
> know that *at least* one of A or B must be true while still not knowing
> the truth value of either. These sorts of things occur all the time.
>

That is not true. If A and B are syntactically correct expressions of a
formal language yet neither one is semantically correct then we have the
same case as the Liar Paradox not being a truth bearer, thus (A ∨ B) is
neither true nor false.

> And not being provable in PA and not being provable are also two
> different things.
>

I know that. Yet not being provable in PA also means that G cannot be
derived in PA by applying truth preserving operations to the axioms Z of
PA or other expressions Y derived from Z or Y.

If G is correctly determined to be true then there must be some process
detailing the steps of how it is 'Correctly determined to be true'.
Lacking these steps one cannot correctly assert that G is true, only
that G might possibly be true.

>>> The question is not whether it is true but whether it is a truth
>>> *bearer*.
>>>
>>> You make the claim that The Liar is not a truth bearer (a plausible
>>> claim depending on one's definitions).
>>>
>>> You then jump to the conclusion that G is not a truth bearer based on
>>> your assertion that it is "equivalent" to The Liar. But it is *NOT*
>>> equivalent. It merely bears a close relationship. But you refuse to
>>> actually consider what the nature of that relationship; there are
>>> both similiarites and differences.
>>>
>>
>> Precise equivalence is defined by this:
>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>
>> The Liar Paradox can be neither proven nor refuted where T is the
>> entire body of analytic knowledge and φ is LP.
>
> The Liar Paradox is a self-contradiction. The Gödel sentence is not.

Until you understand that G can only be correctly asserted to be true in
X if G is provable in X. G may be true in X without a proof in X, yet it
cannot be correctly asserted to be true in X without such a proof.

>
>>> Whereas the Liar has no content other than to assert its own falsity,
>>> Gödel's G has definite content. It does not assert its own
>>> unprovability, it asserts a very specific mathematical claim, one
>>> which must by its nature be either true or false. Therefore G *is* a
>>> truth bearer.
>>>
>>> The formulation that G asserts its own unprovability is the
>>> Cliff-Notes version of the proof. It's not the substance of the
>>> actual proof.
>>>
>>> André
>>
>> It is isomorphic to the substance of the actual proof.
>
> No. It is not. G asserts a claim about mathematics. It does not assert
> anything about itself. However, within the metalanguage we can prove
> that G can only be true if it is not provable within the system under
> consideration.
>

Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
When both G and the LP exactly meet the official mathematical definition
of incompleteness then G and LP are proven to be isomorphic.

>> Gödel says:
>> since the undecidable proposition [R(q); q] states precisely that q
>> belongs to K, i.e. according to (1), that [R(q); q] is not provable.
>> We are therefore confronted with a proposition which asserts its own
>> unprovability.
>
> We are confronted *in our analysis* with such a situation. But there is
> no proposition which directly asserts such a thing.
>

You are letting weasel words leak semantic meaning.
My analysis pertaining to the official mathematical definition of
incompleteness cuts through these weasel words.

This proves that G the LP and the following sentence are all isomorphic:
"This sentence is unprovable".

> The problem is you refuse to look at the actual math and instead look
> only at the text commentary which is merely a guide to, not the actual
> substance of, the proof.
>
> André
>

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

On 5/3/2022 1:33 PM, Jeff Barnett wrote:
> On 5/3/2022 9:18 AM, André G. Isaak wrote:
>> On 2022-05-02 18:57, olcott wrote:
>
> IDIOT SNIPPED
>
>
>> No. The Liar can be used to construct an *identical* proof. Other
>> antinomies could be used for similar proofs. He's already talking
>> about The Liar.
>>
>>> Which means that the Liar Paradox is sufficiently equivalent to
>>> Gödel's G. Which means if the basic mechanism of epistemological
>>> antinomy is shown to be semantically incorrect then Gödel's G is
>>> shown to be semantically incorrect.
>>
>> You have some serious reading comprehension problems. I never denied
>> the things Gödel wrote. I denied your conclusion because it does not
>> follow.
>>
>> Gödel starts by claiming there is a close relationship (*not*
>> equivalence) between one particular antinomy, The Liar, and his G.
>>
>> He then states that similar proofs could be constructed using any
>> antinomy.
>>
>> That entails that other antinomies could be used to construct similar
>> proofs involving a similar close relation (again, *not* equivalence).
>>
>> Gödel never claims *any* antinomy is equivalent to his G. Merely that
>> a close relationship holds.
>>
>> And all my comments concerned exactly what that relationship is.
> I think that you have provided the troll a similar explanation over 100
> times. I admire your tenacity but I must ask you a question: Why do you
> think one more time will do either him or you any good? It's not like
> this is an educational or soul-improving opportunity for either of you;
> for you this must be frustrating no matter your intentions and for him
> he is what he is and this is his only amusement. Whether troll or
> buffoon, he's proud of his appearance as wasted space.

Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
I used the above as the precise measure of isomorphism.

The whole error of the incompleteness theorem is entirely anchored in
that the official mathematical definition of incompleteness incorrectly
presumes that syntactically correct expressions of the language of
formal system T are necessarily also semantically incorrect.

When T is the entire body of analytic knowledge and φ is the liar
paradox, the official mathematical definition of incompleteness
determines that the entire body of analytic knowledge is incomplete.

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

On 2022-05-03 13:12, olcott wrote:

> When T is the entire body of analytic knowledge and φ is the liar
> paradox, the official mathematical definition of incompleteness
> determines that the entire body of analytic knowledge is incomplete.

G is not a formalization of The Liar. There is no such formalization in
the systems Gödel considers.

The Liar results in inconsistency whereas G results in incompleteness.
This is a major difference between G and The Liar which is why you need
to stop conflating the two. The Liar only exists in natural language,
not in mathematics.

André

--
To email remove 'invalid' & replace 'gm' with well known Google mail
service.

On 5/3/2022 9:59 AM, Ben wrote:
> olcott <polcott2@gmail.com> writes:
>
>> On 5/2/2022 9:21 PM, Ben wrote:
>>> olcott <polcott2@gmail.com> writes:
>>>
>>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>
>>>>>> Thanks for confirmation, that's what exactly what I was trying to tell
>>>>>> to topic poster in one of my previous posts. Prolog in it's bare form
>>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>>
>>>>>> If you want to deal with such problems maybe it is better to use Coq
>>>>>> theorem prover, I've never used it by myself, but it looks like one of
>>>>>> the best proving assistants out there.
>>>>>
>>>>> And indeed there is a fully formalised proof of GIT in Coq (though I
>>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>
>>>> It is true that G is not provable.
>>> G is provable. Proofs abound. I was pointing out one in a proper proof
>>> assistant, Coq.
>>
>> It is OK that you are not a math guy.
>
> You are not a math guy. I am.
>
>> If you were a math guy you would understand that if G is provable then
>> that makes Gödel totally wrong. G is not Gödel's theorem, it is a key
>> element of his theorem.
>
> No. G is provable. Though I did make a mistake -- the link was to a
> proof of G-RIT not G.
>
> How are you getting on with E and specifying P? Have you given up?
>

The barest skeleton of my {Simplest TM interpreter} is complete.
I usually have a copy of the skeleton for reading the lines of a text
file, I had to recreate this one from scratch.

The next step is to make the detailed design.
I am shooting to complete the whole project in four labor hours from
now. I excluded the tedious syntax related aspects of the text file
reader because this always takes far too long.

#include <iostream>
#include <fstream>
#include <string>

inline void Outlines(std::string FileName)
{ std::string Line;
std::ifstream fin;

fin.open(FileName.c_str());
if (!fin.is_open())
{
std::cout << FileName << " " << "Does Not Exist!";
return;
}
while (std::getline(fin, Line))
{
printf("%s\n", Line.c_str());
}
fin.close();
}

int main(int argc, char *argv[])
{ if (argc != 2)
printf("Must provide Filename\n");
else
Outlines(argv[1]);
}

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

On 2022-05-03 12:59, olcott wrote:
> On 5/3/2022 1:23 PM, André G. Isaak wrote:
>> On 2022-05-03 11:33, olcott wrote:
>>> On 5/3/2022 12:17 PM, André G. Isaak wrote:
>>>> On 2022-05-03 11:05, olcott wrote:
>>>>> On 5/3/2022 11:52 AM, André G. Isaak wrote:
>>
>> <snippage>
>>
>>>>>> G is very clearly a truth-bearer. Go back and reread my original
>>>>>> explanation.
>>>>>>
>>>>>
>>>>> When G is not provable in PA, how is it shown to be true?
>>>>> If it is not shown to be true in PA then we have the strawman error.
>>>>
>>>> Here you're simply begging the question by assuming your own
>>>> conclusion: that being true and being provable are the same.
>>>
>>> This is not any mere assumption.
>>>
>>> The only way that any analytic expressions of language are correctly
>>> determined to be true is:
>>
>> 'True' and 'Correctly determined to be true' mean different things.
>>
>
> Yes that seems to be correct.
> On the other hand calling an expression of language true that has not be
> 'Correctly determined to be true' is an error.

But calling it a "non-truth bearer" simply because it has not been
determined to be true would equally be an error.

And it can be shown (i.e. correctly determined) that G is true, just not
within the system for which it was constructed.

> If G is claimed to be true then this assertion must be supported by:
> 'Correctly determined to be true' otherwise the assessment of its truth
> is no more than a wild guess.
>
>>> (a) They are defined to be true.
>>> (b) They are derived from applying truth preserving operations to (a)
>>> or (b). Prolog knows this on the basis of its facts and rules. Facts
>>> are (a) and rules are (b). This is also known as sound deductive
>>> inference.
>>
>> These are YOUR assumptions. They have not been demonstrated. And they
>> are not consistent with the way in which the rest of the world talks
>> about truth. You are talking about provability, not truth.
>>
>
> If G is claimed to be true then this assertion must be supported by:
> 'Correctly determined to be true' otherwise the assessment of its truth
> is no more than a wild guess.
>
>>>> The whole point of Gödel's proof is that they cannot be the same (at
>>>> least not for non-trivial systems).
>>>>
>>>
>>> When G is not provable in PA, how is it shown to be true (wild guess)?
>>> What is the precise basis for assessing that G is true? please
>>> provide ALL the steps.
>>
>> "True" and "Known to be true" are entirely different things.
>>
>
> Yes, however:
> If G is claimed to be true then this assertion must be supported by:
> 'Correctly determined to be true' otherwise the assessment of its truth
> is no more than a wild guess.

As I said, it can be shown in a higher order system.

But even if it could not be, if we can show that G can only be true in
cases where it is not provable in T, then there are only two possible
conclusions:

Either G is true and unprovable in T, in which case T is incomplete.
Or G is false and provable in T, in which case T is inconsistent.

Which is exactly what Gödel's theorem states: A system can be consistent
or it can be complete but it cannot be both. An incomplete system is
still useful. An inconsistent system is not. Ergo he phrases this as an
consistent system must be incomplete [with the usual caveats about
meeting some minimum threshold of expressive power].

>> Consider the equation Srt((2748 + 87)^3) = 150,948.776 (to 3 decimal
>> places)
>>
>
> (2748 + 87)^3 = 22,785,532,875
> What are you sorting with Srt()?

That was obviously a type. Sqrt().

>> That equation is true but it is unlikely anyone knew this to be true
>> until now since I very much doubt anyone had previously considered
>> that specific equation. That's doesn't mean it wasn't true all along.
>> Just that no one knew it was true.
>>
>> There are all sorts of cases where we know one thing without knowing
>> all things. I can know with certainty that (A ∨ B) is true meaning
>> that I know that *at least* one of A or B must be true while still not
>> knowing the truth value of either. These sorts of things occur all the
>> time.
>>
>
> That is not true. If A and B are syntactically correct expressions of a
> formal language yet neither one is semantically correct then we have the
> same case as the Liar Paradox not being a truth bearer, thus (A ∨ B) is
> neither true nor false.

But your whole notion of 'semantically correct' is recognized by no one
but you and is antithetical to the entire notion of a formal system. And
what I describe above is a situation which *very* commonly arises in
proofs. They're called proofs by dilemma and take the form:

A → C
B → C
(A ∨ B)

Therefore C

We draw a conclusion from A or B without knowing the truth value of
either. This strategy, for example, was used by Euclid in his proof that
no largest prime exists.

If you declare A and B to be 'non-truth bearers' simply because you
don't know whether they are true or false, then this and many other
proofs completely fall apart.

>> And not being provable in PA and not being provable are also two
>> different things.
>>
>
> I know that. Yet not being provable in PA also means that G cannot be
> derived in PA by applying truth preserving operations to the axioms Z of
> PA or other expressions Y derived from Z or Y.
>
> If G is correctly determined to be true then there must be some process
> detailing the steps of how it is 'Correctly determined to be true'.

Just not in PA.

> Lacking these steps one cannot correctly assert that G is true, only
> that G might possibly be true.
>
>>>> The question is not whether it is true but whether it is a truth
>>>> *bearer*.
>>>>
>>>> You make the claim that The Liar is not a truth bearer (a plausible
>>>> claim depending on one's definitions).
>>>>
>>>> You then jump to the conclusion that G is not a truth bearer based
>>>> on your assertion that it is "equivalent" to The Liar. But it is
>>>> *NOT* equivalent. It merely bears a close relationship. But you
>>>> refuse to actually consider what the nature of that relationship;
>>>> there are both similiarites and differences.
>>>>
>>>
>>> Precise equivalence is defined by this:
>>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>>
>>> The Liar Paradox can be neither proven nor refuted where T is the
>>> entire body of analytic knowledge and φ is LP.
>>
>> The Liar Paradox is a self-contradiction. The Gödel sentence is not.
>
> Until you understand that G can only be correctly asserted to be true in
> X if G is provable in X. G may be true in X without a proof in X, yet it
> cannot be correctly asserted to be true in X without such a proof.

This is your confusion, not mine. We can assert that G is not provable
and that ¬G is also not provable without asserting anything at all about
whether G is true and still conclude that X is incomplete.

>>
>>>> Whereas the Liar has no content other than to assert its own
>>>> falsity, Gödel's G has definite content. It does not assert its own
>>>> unprovability, it asserts a very specific mathematical claim, one
>>>> which must by its nature be either true or false. Therefore G *is* a
>>>> truth bearer.
>>>>
>>>> The formulation that G asserts its own unprovability is the
>>>> Cliff-Notes version of the proof. It's not the substance of the
>>>> actual proof.
>>>>
>>>> André
>>>
>>> It is isomorphic to the substance of the actual proof.
>>
>> No. It is not. G asserts a claim about mathematics. It does not assert
>> anything about itself. However, within the metalanguage we can prove
>> that G can only be true if it is not provable within the system under
>> consideration.
>>
>
> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
> When both G and the LP exactly meet the official mathematical definition
> of incompleteness then G and LP are proven to be isomorphic.

On 5/3/2022 1:12 PM, olcott wrote:
> On 5/3/2022 1:33 PM, Jeff Barnett wrote:
>> On 5/3/2022 9:18 AM, André G. Isaak wrote:
>>> On 2022-05-02 18:57, olcott wrote:
>>
>> IDIOT SNIPPED
>>
>>
>>> No. The Liar can be used to construct an *identical* proof. Other
>>> antinomies could be used for similar proofs. He's already talking
>>> about The Liar.
>>>
>>>> Which means that the Liar Paradox is sufficiently equivalent to
>>>> Gödel's G. Which means if the basic mechanism of epistemological
>>>> antinomy is shown to be semantically incorrect then Gödel's G is
>>>> shown to be semantically incorrect.
>>>
>>> You have some serious reading comprehension problems. I never denied
>>> the things Gödel wrote. I denied your conclusion because it does not
>>> follow.
>>>
>>> Gödel starts by claiming there is a close relationship (*not*
>>> equivalence) between one particular antinomy, The Liar, and his G.
>>>
>>> He then states that similar proofs could be constructed using any
>>> antinomy.
>>>
>>> That entails that other antinomies could be used to construct similar
>>> proofs involving a similar close relation (again, *not* equivalence).
>>>
>>> Gödel never claims *any* antinomy is equivalent to his G. Merely that
>>> a close relationship holds.
>>>
>>> And all my comments concerned exactly what that relationship is.
>> I think that you have provided the troll a similar explanation over
>> 100 times. I admire your tenacity but I must ask you a question: Why
>> do you think one more time will do either him or you any good? It's
>> not like this is an educational or soul-improving opportunity for
>> either of you; for you this must be frustrating no matter your
>> intentions and for him he is what he is and this is his only
>> amusement. Whether troll or buffoon, he's proud of his appearance as
>> wasted space.
>
> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
> I used the above as the precise measure of isomorphism.
>
> The whole error of the incompleteness theorem is entirely anchored in
> that the official mathematical definition of incompleteness incorrectly
> presumes that syntactically correct expressions of the language of
> formal system T are necessarily also semantically incorrect.
>
> When T is the entire body of analytic knowledge and φ is the liar
> paradox, the official mathematical definition of incompleteness
> determines that the entire body of analytic knowledge is incomplete.
Polly want a cracker?
--
Jeff Barnett

Peter Olcott wrote:
....
> The barest skeleton of my {Simplest TM interpreter} is complete.
> I usually have a copy of the skeleton for reading the lines of a text
> file, I had to recreate this one from scratch.
>
> The next step is to make the detailed design.
> I am shooting to complete the whole project in four labor hours from
> now. I excluded the tedious syntax related aspects of the text file
> reader because this always takes far too long.
>
> #include <iostream>
> #include <fstream>
> #include <string>
>
>
> inline void Outlines(std::string FileName)
> {
>   std::string Line;
>   std::ifstream fin;
>
>   fin.open(FileName.c_str());
>   if (!fin.is_open())
>   {
>     std::cout << FileName << " " << "Does Not Exist!";
>     return;
>   }
>   while (std::getline(fin, Line))
>   {
>     printf("%s\n", Line.c_str());
>   }
>   fin.close();
> }
>
>
> int main(int argc, char *argv[])
> {
>   if (argc != 2)
>     printf("Must provide Filename\n");
>   else
>     Outlines(argv[1]);
> }

It is a joke, right?

On 5/3/2022 4:58 PM, Jeff Barnett wrote:
> On 5/3/2022 1:12 PM, olcott wrote:
>> On 5/3/2022 1:33 PM, Jeff Barnett wrote:
>>> On 5/3/2022 9:18 AM, André G. Isaak wrote:
>>>> On 2022-05-02 18:57, olcott wrote:
>>>
>>> IDIOT SNIPPED
>>>
>>>
>>>> No. The Liar can be used to construct an *identical* proof. Other
>>>> antinomies could be used for similar proofs. He's already talking
>>>> about The Liar.
>>>>
>>>>> Which means that the Liar Paradox is sufficiently equivalent to
>>>>> Gödel's G. Which means if the basic mechanism of epistemological
>>>>> antinomy is shown to be semantically incorrect then Gödel's G is
>>>>> shown to be semantically incorrect.
>>>>
>>>> You have some serious reading comprehension problems. I never denied
>>>> the things Gödel wrote. I denied your conclusion because it does not
>>>> follow.
>>>>
>>>> Gödel starts by claiming there is a close relationship (*not*
>>>> equivalence) between one particular antinomy, The Liar, and his G.
>>>>
>>>> He then states that similar proofs could be constructed using any
>>>> antinomy.
>>>>
>>>> That entails that other antinomies could be used to construct
>>>> similar proofs involving a similar close relation (again, *not*
>>>> equivalence).
>>>>
>>>> Gödel never claims *any* antinomy is equivalent to his G. Merely
>>>> that a close relationship holds.
>>>>
>>>> And all my comments concerned exactly what that relationship is.
>>> I think that you have provided the troll a similar explanation over
>>> 100 times. I admire your tenacity but I must ask you a question: Why
>>> do you think one more time will do either him or you any good? It's
>>> not like this is an educational or soul-improving opportunity for
>>> either of you; for you this must be frustrating no matter your
>>> intentions and for him he is what he is and this is his only
>>> amusement. Whether troll or buffoon, he's proud of his appearance as
>>> wasted space.
>>
>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>> I used the above as the precise measure of isomorphism.
>>
>> The whole error of the incompleteness theorem is entirely anchored in
>> that the official mathematical definition of incompleteness
>> incorrectly presumes that syntactically correct expressions of the
>> language of formal system T are necessarily also semantically incorrect.
>>
>> When T is the entire body of analytic knowledge and φ is the liar
>> paradox, the official mathematical definition of incompleteness
>> determines that the entire body of analytic knowledge is incomplete.
> Polly want a cracker?

In other words you have no rebuttal either because what I said is over
your head or you want to make sure to never agree that I correctly
proved my point. I vote for both.

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

On 5/3/2022 5:13 PM, Python wrote:
> Peter Olcott wrote:
> ...
>> The barest skeleton of my {Simplest TM interpreter} is complete.
>> I usually have a copy of the skeleton for reading the lines of a text
>> file, I had to recreate this one from scratch.
>>
>> The next step is to make the detailed design.
>> I am shooting to complete the whole project in four labor hours from
>> now. I excluded the tedious syntax related aspects of the text file
>> reader because this always takes far too long.
>>
>> #include <iostream>
>> #include <fstream>
>> #include <string>
>>
>>
>> inline void Outlines(std::string FileName)
>> {
>>    std::string Line;
>>    std::ifstream fin;
>>
>>    fin.open(FileName.c_str());
>>    if (!fin.is_open())
>>    {
>>      std::cout << FileName << " " << "Does Not Exist!";
>>      return;
>>    }
>>    while (std::getline(fin, Line))
>>    {
>>      printf("%s\n", Line.c_str());
>>    }
>>    fin.close();
>> }
>>
>>
>> int main(int argc, char *argv[])
>> {
>>    if (argc != 2)
>>      printf("Must provide Filename\n");
>>    else
>>      Outlines(argv[1]);
>> }
>
> It is a joke, right?
>
>

This is a file that only reads and outputs text lines, thus provides the
skeleton for my Simplest TM interpreter. I almost always have some code
that I can cut-and-paste this from. I couldn't find it so I had to
create this from scratch.

I count this as my starting point for my Simplest TM interpreter. I want
to see if I can get the entire project completed in less that four
hours, including detailed design, coding and debugging and not including
user documentation. So far I made great progress on the detailed design
in two minutes.

It is based on the design of this system yet much simpler:
http://www.lns.mit.edu/~dsw/turing/turing.html

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