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

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.

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

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.

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