Path: news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail From: Mikko Newsgroups: sci.logic Subject: Re: The key undecidable instance that I know about --- Truth-bearers ONLY Date: Fri, 21 Mar 2025 11:06:42 +0200 Organization: - Lines: 142 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: Fri, 21 Mar 2025 10:06:42 +0100 (CET) Injection-Info: dont-email.me; posting-host="cae169de1f4b106dcdbefb0dc8de4776"; logging-data="1302632"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/tnz0l6GtaD6N4w7CK59+3" User-Agent: Unison/2.2 Cancel-Lock: sha1:Vwi3ncR2JVSjDxBnqg+eXxLLsCI= 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 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