Re: The key undecidable instance that I know about

On 3/10/2025 4:48 AM, Mikko wrote:

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.
 

I created Minimal Type Theory such that self-reference
can be expressed concisely and correctly. Apparently
this cannot be expressed concisely and correctly in
any formal logic system.
Here is how this is typically done in formal systems
2.4 Diagonalization, or, “Self-reference”
https://plato.stanford.edu/entries/goedel-incompleteness/#DiaSelRef
LP := ~True(LP) is exactly self-reference without the
convoluted mess of the The Diagonalization Lemma.
The other advantage of Minimal Type Theory is that
it outputs a directed graph of the evaluation sequence
explicitly showing any cycles that prove the expression
is invalid in the exact same way that
?- unify_with_occurs_check(LP, not(true(LP))).
proves that LP = not(true(LP)). has a cycle in its
evaluation sequence.

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

In other words you can see the infinite structure of:
?- LP = not(true(LP)).
Not checking for cycles This is the default because
checking for cycles is too costly.

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.
 

Proving a cycle in the evaluation sequence of ?- LP = not(true(LP)).

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.

Proving that ?- LP = not(true(LP)). is infinitely recursive.

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.
 

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