Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail
From: olcott <polcott333@gmail.com>
Newsgroups: sci.logic
Subject: Re: The key undecidable instance that I know about --- Truth-bearers
 ONLY
Date: Wed, 19 Mar 2025 18:22:53 -0500
Organization: A noiseless patient Spider
Lines: 144
Message-ID: <vrfjkd$1s64t$1@dont-email.me>
References: <vqkib1$r5np$1@dont-email.me>
 <3b57384a57c71e1880fe3f1df975003c1d743c07@i2pn2.org>
 <vqksgr$sf7f$2@dont-email.me>
 <c2a4c70287c029f462d5579a8602746386f546fc@i2pn2.org>
 <vql4mq$uv13$1@dont-email.me>
 <9a2fbcc7a803bc91d320117f8c8e03e03799e9b3@i2pn2.org>
 <vqlmtf$11p4p$2@dont-email.me>
 <95ca0b344ae29f6911a73c655ddbe1c7214f8519@i2pn2.org>
 <vqo4ke$1l6i0$1@dont-email.me>
 <c5b83ef1ae7f77e3ff1fe97dcb557af5380c2ddd@i2pn2.org>
 <vqo7or$1l6i0$3@dont-email.me> <vqo8bf$1lehl$1@dont-email.me>
 <vr4c6h$3u6l5$1@dont-email.me> <vr8oq5$3qi1v$1@dont-email.me>
 <vr97q9$6vsn$2@dont-email.me> <vrbvfv$2lq1i$1@dont-email.me>
 <vrd803$3oqkg$1@dont-email.me> <vreph9$16e25$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 20 Mar 2025 00:22:54 +0100 (CET)
Injection-Info: dont-email.me; posting-host="ca94344bd24a354eba3539b74c3bed05";
	logging-data="1972381"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+0/jh4lBwsuNj1Q7VIuIUI"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:y3vwUt3hBGF6FCH73uAMZ7krw0E=
In-Reply-To: <vreph9$16e25$1@dont-email.me>
X-Antivirus: Norton (VPS 250319-10, 3/19/2025), Outbound message
X-Antivirus-Status: Clean
Content-Language: en-US
Bytes: 7739

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