XPost: comp.lang.c, comp.lang.c++, comp.lang.prolog   
   From: polcott333@gmail.com   
      
   int DD()   
   {   
     int Halt_Status = HHH(DD);   
     if (Halt_Status)   
     HERE: goto HERE;   
     return Halt_Status;   
   }   
      
   HHH simulates DD step-by-step according to the   
   semantics of the C programming language.   
      
   HHH correctly determines that DD does not have   
   a well-founded justification tree within Proof   
   theoretic semantics.   
      
   When HHH is construed as a proof theoretic halting   
   prover HHH detects the pathological self-reference   
   of its input and rejects DD as non-well-founded on   
   this basis.   
      
   % This sentence is not true.   
   ?- LP = not(true(LP)).   
   LP = not(true(LP)).   
   ?- unify_with_occurs_check(LP, not(true(LP))).   
   false.   
      
   The Liar Paradox is formally rejected by Prolog   
   occurs_check for this same reason.   
      
   occurs_check correctly determines that LP does not   
   have a well-founded justification tree within Proof   
   theoretic semantics   
      
      
      
      
   All five LLM systems agree with the above   
   this one is the most succinct agreement:   
      
   *Halting Problem and Proof Theoretic Semantics*   
   https://philpapers.org/archive/OLCHPA.pdf   
      
   https://philpapers.org/rec/OLCHPA   
      
   https://www.researchgate.net/publication/400341134_Halting_Probl   
   m_and_Proof_Theoretic_Semantics   
      
   --   
   Copyright 2026 Olcott

   
      
   My 28 year goal has been to make 
   
   "true on the basis of meaning expressed in language"
   
   reliably computable for the entire body of knowledge.

   
      
   This required establishing a new foundation
   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)