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

On 3/19/2025 10:57 AM, Mikko wrote:

On 2025-03-19 01:52:01 +0000, olcott said:
 

On 3/18/2025 9:20 AM, Mikko wrote:

On 2025-03-17 13:24:24 +0000, olcott said:
>

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

On 2025-03-15 17:08:33 +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
LP := ~True(LP) resolves to true
>
Therefore the assumption that a correct True() predicate exists is proven false.

>
When you stupidly ignore Prolog and MTT that
both prove there is a cycle in the directed graph
of their evaluation sequence. If you have no idea
what "cycle", "directed graph" and "evaluation sequence"
means then this mistake is easy to make.

>
Prolog does not prove anything other than what you ask. I don't think
you can ask Prolog whether there is a cycle in LP after LP = not(true(LP)).

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

>
Meaning that LP = not(true(LP)) is accepted as a valid query and evalated
as true with the implication that LP is the same as not(true(LP)).
>

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

>
Meaning that unify_with_occurs_check(LP, not(true(LP))) is accepted as a
valid query and evaluated as false.

>
I have been saying "cycles" all along and it has always been cycles.

 Not all along, just occasionally. What you did say that Prolog proves
that there is a cycle in the directed graph of their evaluation sequence.
I said that Prolog does not prove that. Then you posted some examples of
prolog not proving that and didn't mention "cycles" any more.
 

https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2

 That link confirms what I said above. It also said that one of the arguments
already has a cycle then that cycle does not prevent unification and does
not cause infinite execution.
 

Clearly you have no idea what a cycle in a directed graph means.
In an evaluation sequence it means infinite loop.
Meaning that undetected cycles cause infinite loops.
In the context of Prolog and term manipulation, a "cyclic term" or "rational tree" refers to a term where a variable can be unified with a subterm that, directly or indirectly, contains the same variable, creating a circular structure. [1, 2, 3]
Here's a more detailed explanation: [1, 2, 3]
• Cyclic Terms/Rational Trees: These are terms that can be represented as a tree structure where a node can point back to itself or to a node that eventually leads back to itself, forming a cycle.
• Example: Consider the term X = f(X). Here, the variable X is unified with a term f(X), where X appears again within that term, creating a cycle.
• Prolog and Unification: In Prolog, unification is the process of finding values for variables that make two terms equal. Unification with cyclic terms can lead to infinite loops if not handled properly.
• SWI-Prolog: SWI-Prolog supports rational trees and provides built-in predicates that can handle them efficiently.
• unify_with_occurs_check/2: This predicate in SWI-Prolog is designed to prevent the creation of cycles during unification. It checks if a variable occurs in the term it's being unified with, and if so, the unification fails.
• Early Prolog Implementations: In older Prolog implementations, the "occurs check" was often omitted for efficiency, leading to potential infinite loops when dealing with cyclic terms.
Generative AI is experimental.
[1] https://www.swi-prolog.org/pldoc/man?section=cyclic[2] https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2[3] https://link.springer.com/content/pdf/10.1007/978-3-662-05138-2_10
--
Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer