Re: The key undecidable instance that I know about

On 2025-03-09 17:15:13 +0000, olcott said:

Is the Liar Paradox True or False?
 LP := ~True(LP)

In typical languages of formal logic that is not a syntactically valid
expression.

?- LP = not(true(LP)).
LP = not(true(LP)).

Apparently you were using a Prolog implementation that does not check
whether a cyclic data structure is produced. Another Prolog implementation
could say false instead.

?- unify_with_occurs_check(LP, not(true(LP))).
false.

For this quesry the only permitted answer is false.

Its infinitely recursive structure makes it neither true nor false.

What is that "its" intended to refer to? According to Prolog rules
unify_with_occurs_check(LP, not(true(LP))) is false. Accordint to
the implementation you were using LP = not(true(LP)) is true but
another implementation might say it is false. If you mean LP itself,
that is neither true nor false just lke 42 is neither true nor false.
--
Mikko