XPost: comp.theory, sci.logic, sci.math   
   From: polcott333@gmail.com   
      
   On 12/1/2025 8:45 AM, Tristan Wibberley wrote:   
   > On 26/11/2025 20:07, olcott wrote:   
   >> On 11/26/2025 1:46 PM, Tristan Wibberley wrote:   
   >>> On 26/11/2025 15:27, olcott wrote:   
   >>>> This is formalized in the Prolog programming language   
   >>>> ?- LP = not(true(LP)).   
   >>>> LP = not(true(LP)).   
   >>>> ?- unify_with_occurs_check(LP, not(true(LP))).   
   >>>> false.   
   >>>   
   >>> Why do you keep posting that?   
   >>>   
   >>   
   >> Until it is accepted or someone correctly shows   
   >> how it does not once-and-for-all resolve   
   >> the Liar Paradox I will keep posting it.   
   >   
   > Can you show how it /does/ ?   
   >   
      
   Been there done that many times no one cares.   
      
   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 so on. So Y ends up standing for some kind of infinite structure.   
   END:(Clocksin & Mellish 2003:254)   
      
   LP = not(true(LP)).   
   not(true(not(true(not(true(not(true(LP)))))))).   
   expands to not(true(not(true(not(true(not(true(...)))))))).   
      
   --   
   Copyright 2025 Olcott   
      
   My 28 year goal has been to make   
   "true on the basis of meaning" computable.   
      
   This required establishing a new foundation   
   for correct reasoning.   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)