Re: The key undecidable instance that I know about

On 3/9/2025 2:24 PM, Richard Damon wrote:

On 3/9/25 1:15 PM, olcott wrote:

Is the Liar Paradox True or False?
>
LP := ~True(LP)
>
?- LP = not(true(LP)).
LP = not(true(LP)).
>
?- unify_with_occurs_check(LP, not(true(LP))).
false.
>
Its infinitely recursive structure makes it neither true nor false.
>

  The liar's paradox isn't an "undecidable" instance, as "undecidable" is about a problem that has a true or false answer that can not be computed for every case.
 

Tarski thought that is was undecidable and anchored his
whole proof in it.
Tarski's Liar Paradox from page 248
    It would then be possible to reconstruct the antinomy of the liar
    in the metalanguage, by forming in the language itself a sentence
    x such that the sentence of the metalanguage which is correlated
    with x asserts that x is not a true sentence.
    https://liarparadox.org/Tarski_247_248.pdf
Formalized as:
x ∉ True if and only if p
where the symbol 'p' represents the whole sentence x
He never shows the above intermediate step before
he arbitrarily swaps True for Provable on line (1)
of his proof in the first paragraph of this proof.
(1) x ∉ Provable and only if p
   In accordance with the first part of Th. I
   we can obtain the negation of one of the
   sentences in condition (ex) of convention
   T of § 3 as a consequence of the definition of
   the symbol 'Pr' (provided we replace 'Tr' in
   this convention by 'Pr').
   https://liarparadox.org/Tarski_275_276.pdf
--
Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer