Re: The key undecidable instance that I know about

On 3/11/2025 6:15 AM, Mikko wrote:

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?
 

https://www.researchgate.net/publication/315367846_Minimal_Type_Theory_MTT
https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF https://www.researchgate.net/publication/317953772_Provability_with_Minimal_Type_Theory
We need such a language so that we don't stupidly
fail to understands how this can convert expressions
of language into non-truth-bearers having no truth value.
Until we do this we get confused into believing
that such expressions are in any way undecidable.

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.
 

LP := ~True(LP)
has all of its semantics encoded in its syntax, thus no
interpretation required.

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?
 

Minimal Type Theory was the only language that I knew
of that could express pathological self-reference correctly.
Years later after I read Clocksin & Mellish I found that
Prolog can do the same thing.

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.
 

Sources said that this is far too costly in terms of
machine cycles thus turned off by default.

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.
 

WRONG carefully study the whole C&M quote
however many times over and over until
you totally get it.

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.
 

*That you keep ignoring it is either stupid or dishonest*
    As a result, Y will stand forfoo(Y), which is
    foo(foo(Y)) (because of what Y stands for),
    which is foo(foo(foo(Y))), and so on. So Y ends
    up standing for some kind of infinite structure.
I am about to write you off as dishonest and never
bother to look at any of your replies again.
--
Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer