Re: The key undecidable instance that I know about --- Truth-bearers ONLY

On 2025-03-20 22:55:17 +0000, olcott said:

On 3/20/2025 7:57 AM, Mikko wrote:

On 2025-03-17 13:18:42 +0000, olcott said:
 

On 3/17/2025 4:04 AM, Mikko wrote:

On 2025-03-16 14:38:16 +0000, olcott said:
 

On 3/16/2025 8:19 AM, Mikko wrote:

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

On 3/11/2025 5:50 AM, Mikko wrote:

On 2025-03-11 03:23:51 +0000, olcott said:
 

On 3/10/2025 9:49 PM, dbush wrote:

On 3/10/2025 10:39 PM, olcott wrote:

On 3/10/2025 9:21 PM, Richard Damon wrote:

On 3/10/25 9:45 PM, olcott wrote:

On 3/10/2025 5:45 PM, Richard Damon wrote:

On 3/9/25 11:39 PM, olcott wrote:

 LP := ~True(LP)  DOES SPECIFY INFINITE RECURSION.

 WHich is irrelevent, as that isn't the statement in view, only what could be shown to be a meaning of the actual statement.
 

 The Liar Paradox PROPERLY FORMALIZED <is> Infinitely recursive
thus semantically incorrect.

 But is irrelevent to your arguement.
 

 "It would then be possible to reconstruct the antinomy of the liar
  in the metalanguage, by forming in the language itself a sentence"

 Right, the "Liar" is in the METALANGUAGE, not the LANGUAGE where the predicate is defined.
 You are just showing you don't understand the concept of Metalanguage.
 

 Thus anchoring his whole proof in the Liar Paradox even if
you do not understand the term "metalanguage" well enough
to know this.

 Yes, there is a connection to the liar's paradox, and that is that he shows that the presumed existance of a Truth Predicate forces the logic system to have to resolve the liar's paradox.
 

 bool True(X)
{
   if (~unify_with_occurs_check(X))
     return false;
   else if (~Truth_Bearer(X))
    return false;
   else
    return IsTrue(X);
}
 LP := ~True(LP)
True(LP) resolves to false.

 ~True(LP) resolves to true

 It may seem that way if you fail to understand
Clocksin & Mellish explanation of
 Most Prolog systems will allow you to
satisfy goals like:
   equal(X, X).
   ?- equal(foo(Y), Y).
 that is, they will allow you to match a
term against an uninstantiated subterm of itself.
 ON PAGE 3
https://www.researchgate.net/ publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence 

 That you can quote some text but don't say anything about it supports the
hypthesis that you don't understand the text you quoted.

 I said that unify_with_occurs_check() detects
cycles in the directed graph of the evaluation
sequence of an expression that does explain
everything even if it seems like I said
blah, blah, blah to everyone not knowing the
meaning of these words: "cycle", directed graph"
"evaluation sequence".

 The above is irrelevant to the fact that you didn't say anothing about
the text you quoted.
 

 LP := ~True(LP) expanded to infinite recursion
~True(~True(~True(~True(~True(~True(...))))))
The same way that Clocksin and Mellish do on their example
that you dishonestly keep ignoring.

 They don't say so in the above quoted text. What they do say is essentially
what I have said in another context but not relevant here.
 

 *It seems to me that you are dishonest abut that*

 Doesn't matter. Hopefully readers can see that you are dishonest but
that is their problem, not yours or mine.
 

BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs from the unification used in Resolution. Most Prolog systems will allow you to satisfy goals like:
   equal(X, X).
   ?- equal(foo(Y), Y).
 that is, they will allow you to match a term against an uninstantiated subterm of itself. In this example, foo(Y) is matched against Y, which appears within it. As a result, Y will stand for foo(Y), which is foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))), and soon. So Y ends up standing for some kind of infinite structure.
END:(Clocksin & Mellish 2003:254)

 The above quote is irrelevant to the question whether ~True(LP) resolves
to true.
 

 If ?- equal(foo(Y), Y)
resolves to foo(foo(foo(foo(foo(foo(...))))))
 then ?- LP = not(true(LP)).
resolves to not(true(not(true(not(true(not(true(...))))))))

Of cours. But that is irrelevant to the fact that you quoted a text
without saying anything about it.
--
Mikko