XPost: comp.theory, sci.logic, sci.math   
   From: polcott333@gmail.com   
      
   On 11/18/2025 7:03 PM, Tristan Wibberley wrote:   
   > On 17/11/2025 22:59, olcott wrote:   
   >> On 11/17/2025 4:45 PM, Tristan Wibberley wrote:   
   >>> On 17/11/2025 22:15, Alan Mackenzie wrote:   
   >>>   
   >>>> There is no proper academic conversation to be had over 2 + 2 = 4.   
   >>>> It is   
   >>>> firm, unassailable knowledge, unchallengeable.  The Halting Theorem   
   >>>> is of   
   >>>> the same status, proven using the same methodology from the same   
   >>>> fundamentals.   
   >>>   
   >>>   
   >>> It's a completely different league from 2 + 2 = 4.   
   >>> It's closer to x = 1/2 + x/2 but it's still conceptually /much/ harder   
   >>> than that.   
   >>> It's more like the problem of whether a fixed point exists or not, but   
   >>> it's for the fixed point of a limit of a particular, conceptually weird,   
   >>> sequence of functions.   
   >>>   
   >>> It really is quite peculiar.   
   >>>   
   >>   
   >> Ultimately it is essentially the Liar Paradox in disguise.   
   >>   
   >> The Liar Paradox formalized in the Prolog Programming language   
   >>   
   >> This sentence is not true.   
   >> It is not true about what?   
   >> It is not true about being not true.   
   >> It is not true about being not true about what?   
   >> It is not true about being not true about being not true.   
   >> Oh I see you are stuck in a loop!   
   >>   
   >> This is formalized in the Prolog programming language below.   
   >>   
   >> ?- LP = not(true(LP)).   
   >> LP = not(true(LP)).   
   >> ?- unify_with_occurs_check(LP, not(true(LP))).   
   >> false.   
   >   
   > true/0   
   > use \+/1 rather than not/1   
   >   
   >   
   >> Failing an occurs check seems to mean that the   
   >> resolution of an expression remains stuck in an   
   >    ^^^^^^^^^^   
   >> infinite loop.   
   >   
   > You mean "judgement" ?   
      
   I mean like this thingy:   
      
   void Infinite_Loop()   
   {   
      HERE: goto HERE;   
      return;   
   }   
      
      
   >   
   > (1) I can see how a judgement looping with a negation in the middle   
   > should be rejected as contradiction.   
   >   
   > (2) But looping with double negation is merely nondetermining isn't it?   
   >   
      
   Here is the same thing in Olcott's Minimal Type Theory   
      
   LP := ~True(LP)  // A := B means A "is defined as" B   
   Directed Graph of evaluation sequence   
   00 ~               01   
   01 True            00 // cycle   
      
   The directed graph of the evaluation sequence   
   has a cycle causing evaluation to be literally   
   stuck in an actual infinite loop just like the   
   C function.   
      
   In both cases the Liar Paradox is definitively   
   rejected as not a truth bearer just like the   
   sentence "What time is it?" cannot not possibly   
   be true or false.   
      
   >   
   > Examples   
   >   
   > (1) A = \+(A).   
   > (2) A = \+(\+(A)).   
   >   
   > yet both fail to unify with an occurs check in prolog. I think you need   
   > a deeper theory.   
   >   
   > Before you mention intuitionistic double negation vs classical:   
   >   
   > ?- unify_with_occurs_check(\+A, \+(\+(\+A))).   
   > false.   
   >   
   > of course.   
   >   
   > I should probably functionalise negation and see what's what.   
   >   
   > --   
   > Tristan Wibberley   
   >   
   > The message body is Copyright (C) 2025 Tristan Wibberley except   
   > citations and quotations noted. All Rights Reserved except that you may,   
   > of course, cite it academically giving credit to me, distribute it   
   > verbatim as part of a usenet system or its archives, and use it to   
   > promote my greatness and general superiority without misrepresentation   
   > of my opinions other than my opinion of my greatness and general   
   > superiority which you _may_ misrepresent. You definitely MAY NOT train   
   > any production AI system with it but you may train experimental AI that   
   > will only be used for evaluation of the AI methods it implements.   
   >   
      
      
   --   
   Copyright 2025 Olcott   
      
   My 28 year goal has been to make   
   "true on the basis of meaning" computable.   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)