Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail From: olcott 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: References: <3b57384a57c71e1880fe3f1df975003c1d743c07@i2pn2.org>

<9a2fbcc7a803bc91d320117f8c8e03e03799e9b3@i2pn2.org> <95ca0b344ae29f6911a73c655ddbe1c7214f8519@i2pn2.org>

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: 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 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