Re: The key undecidable instance that I know about

On 2025-03-10 15:36:28 +0000, olcott said:

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.

Have you pbulished that "Minimal Type Theory" or put it to a web page?
Without a pointer to it there is no point to mention it. Of course one
can create a language that can express a self reference but why would
one?

Apparently this cannot be expressed concisely and correctly in
any formal logic system.

A self reference cannot be expressed in an uninterpreted formal language.
Sometimes some symbols and expressions are interpreted to represent
themselves or other symbols or expressions. For example, the symbol 0
of arthmetic can be interpreted to mean the symbol 0 and the term
S0 the sqence of symbols S and 0.

Here is how this is typically done in formal systems
 2.4 Diagonalization, or, “Self-reference”
https://plato.stanford.edu/entries/goedel-incompleteness/#DiaSelRef

Diagonalixation is not what is "typically" done. It is done when
it is useful.

LP := ~True(LP) is exactly self-reference without the
convoluted mess of the The Diagonalization Lemma.

Only in languages that allow the expression. Typical formal languages
either don't have the symbo ":=" or restrict its use so that the
symbol on the left side cannot be used on the right side. In those
languages the expression LP := ~True(LP) does not mean anything.

The other advantage of Minimal Type Theory is that

It does not make sense to say "The other advantage" when you haven't
already identified one. And how do you know there is no third
advantage?

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.

The library predicate unify_with_occurs_check/2 gives the same result
when asked "unify_with_occurs_check(1, 2)". Is there a cycle in the
evaluation sequence of "1 = 2"?

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

Yes, but the unification algorithm of a typical Prolog implementation
creates it without seeing it.

Not checking for cycles This is the default because
checking for cycles is too costly.

And rarely useful.

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

Only if there is a cycle in the evaluation sequence of 1 = 2.

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.

There is nothing infinite there. Everything that can be in a computer's
memory is finite and everthinng a computer does is done in finite time.
--
Mikko