On 5/1/2022 11:15 AM, André G. Isaak wrote:
> On 2022-05-01 09:57, polcott wrote:
>> On 5/1/2022 8:35 AM, André G. Isaak wrote:
>>> On 2022-05-01 05:40, olcott wrote:
>>>> On 5/1/2022 12:34 AM, André G. Isaak wrote:
>>>>> On 2022-04-30 22:49, olcott wrote:
>>>>>> On 4/30/2022 8:53 PM, André G. Isaak wrote:
>>>>>>> On 2022-04-30 19:47, olcott wrote:
>>>>>>>> On 4/30/2022 8:08 PM, Richard Damon wrote:
>>>>>>>>> On 4/30/22 3:02 AM, olcott wrote:
>>>>>>>>>> LP := ~True(LP) is translated to Prolog:
>>>>>>>>>>
>>>>>>>>>> ?- LP = not(true(LP)).
>>>>>>>>>> LP = not(true(LP)).
>>>>>>>>>>
>>>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>> false.
>>>>>>>>>>
>>>>>>>>>> (SWI-Prolog (threaded, 64 bits, version 7.6.4)
>>>>>>>>>>
>>>>>>>>>>
https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> Since it isn't giving you a "syntax error", it is probably
>>>>>>>>> correct Prolog. Not sure if your interpretation of the results
>>>>>>>>> is correct.
>>>>>>>>
>>>>>>>> I asked the question incorrectly, what I really needed to know
>>>>>>>> is whether or not the Prolog correctly encodes this logic sentence:
>>>>>>>> LP := ~True(LP)
>>>>>>>
>>>>>>> Since that isn't a 'logic sentence', no one can answer this.
>>>>>>>
>>>>>>> André
>>>>>>>
>>>>>>>
>>>>>>
>>>>>> What about this one?
>>>>>> LP ↔ ¬True(LP) // Tarski uses something like this
>>>>>
>>>>> That requires that you define some predicate 'True'. Presumably
>>>>> True(LP) must mean something other than LP or it would be purely
>>>>> redundant.
>>>>>
>>>>
>>>> For the purpose of verifying that it is semantically incorrect
>>>> True() can simply be an empty placeholder. The result is that no
>>>> matter how True() is defined the above logic sentence is
>>>> semantically incorrect.
>>>
>>> You're missing my point. Unless you are claiming that there is a
>>> difference between 'x if and only if y' and 'x is true if and only if
>>> y is true', then there is no reason for such a predicate at all. The
>>> fact that you insist on including it suggests you *do* think there is
>>> a difference in meaning between these two examples. So what is that
>>> difference?
>>>
>>> But whatever it means, LP ↔ ¬True(LP) is either simply true or simply
>>> false. It is *not* the liar paradox. Most likely it is simply false
>>> since I assume LP ↔ ¬True(LP) is simply the same as LP ↔ ¬LP.
>>>
>>>>> LP ↔ ¬LP
>>>>>
>>>>> is simply false. It is not a translation of 'This sentence is false'.
>>>>>
>>>>> As a statement of logic, no. As a statement in the metalanguage of
>>>>> logic, sure. As a paraphrase of Gödel, not exactly.
>>>>>
>>>>
>>>> G ↔ ¬Provable(F, G)
>>>
>>> If you want to paraphrase Gödel, you need both G and ⌈G⌉ to be
>>> present in your statement.
>>>
>>> André
>>>
>>
>> That it not what this says:
>> 14 Every epistemological antinomy can likewise be used for a similar
>> undecidability proof
>
> That footnote says absolutely nothing about how to formalize Gödel's
> Theorem.
>
It says that Every epistemological antinomy can likewise be used for a
similar undecidability proof
thus even English epistemological antinomies such as the Liar antinomy
can be used.
Gödel says:
"There is also a close relationship with the “liar” antinomy"
>> G ↔ ¬Provable(F, G) is an epistemological antinomy therefore it is
>> necessarily sufficient.
>
> There is no antinomy involved in that formula, epistemological or
> otherwise.
>
Prolog disagrees.
To boil the Gödel proof down to its bare essence we use the simplest
Liar epistemological antinomy: LP ↔ ¬True(LP)
This way we don't need dozens pages of hundreds of formulas and Prolog
is smart enough to detect and reject it as erroneous.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
False means that LP ↔ ¬True(LP) specifies:
¬True(¬True(¬True(¬True(¬True(¬True(¬True(¬True(¬True(¬True(...))))))))))
(SWI-Prolog (threaded, 64 bits, version 7.6.4)
> If you wish to know how to best formalize Gödel, simply read Gödel; he
> provides the proper formalization for you.
>
>> Likewise with this one: LP ↔ ¬True(LP)
>> It can be evaluated as semantically incorrect without the need to
>> define True(). No matter how True() is defined LP ↔ ¬True(LP) is
>> semantically incorrect.
>
> There's nothing 'semantically incorrect' about it. It evaluates to
> false. It's not the Liar's Paradox.
>
?- unify_with_occurs_check(LP, not(true(LP))).
false.
false means that LP ↔ ¬True(LP) specifies:
¬True(¬True(¬True(¬True(¬True(¬True(¬True(¬True(¬True(¬True(...))))))))))
> The reason I keep asking you to define your 'True' predicate is simply
> that it seems utterly unnecessary and pointless.
Any logic sentence having the self-referential form of the Liar Paradox
specifies infinitely recursive definition, thus is semantically incorrect.
From Clocksin and Mellish:
equal(X, X).?-
equal(foo(Y), Y).
specifies:
foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
> If you believe
> otherwise, then please explain what the difference between the following
> formulae might possibly be:
>
I never waste time carefully examining every possible permutation of an
idea because this would guarantee that I am dead long before my proof is
complete. That I have proved my point with one is them is entirely
sufficient. My example corresponds to the definitive example provided by
the worlds best experts on the Prolog language.
> (1) LP ↔ ¬True(LP)
> (2) True(LP) ↔ ¬True(LP)
> (3) LP ↔ ¬LP
> (4) True(LP) ↔ ¬LP
>
> André