XPost: comp.theory, sci.math, comp.lang.prolog   
   From: polcott333@gmail.com   
      
   Non-programmers and non-Prolog programmers only   
   understand Occurs‑check failure as “Prolog doesn’t like it”.   
      
   When you write LP = not(true(LP)) you are defining LP   
   in terms of itself with no base case. If you try to   
   expand the structure, you get:   
   not(true(not(true(not(true(not(true(…))))))))   
      
   The expansion never bottoms out. It is an infinite   
   regress. Most Prolog systems will show a cyclic term   
   if you run:?- LP = not(true(LP)).   
      
   But this is only a compact representation. It is not   
   a well‑founded term in the ISO sense.   
      
   If you enforce the ISO occurs check:   
   ?- unify_with_occurs_check(LP, not(true(LP))).   
   you get: false.   
      
   Occurs‑check failure has a precise meaning:   
   the unification would create a non‑well‑founded term   
   whose structure expands forever. ISO Prolog requires   
   all terms to be finite and well‑founded, so the   
   unification must fail.   
      
   For non‑Prolog programmers: occurs‑check failure means   
   the system was about to build a data structure that   
   expands forever. No finite machine can represent that   
   safely. If Prolog actually tried to expand it, it would   
   recurse until it ran out of memory. So Prolog correctly   
   rejects it.   
      
   Conclusion: LP = not(true(LP)) is formally ill‑founded   
   in Prolog’s term model. Its structural expansion is   
   infinite, it violates the well‑foundedness requirement for   
   terms, and unify_with_occurs_check/2 correctly detects   
   this. Because the term cannot be well‑founded, it cannot   
   be assigned a truth value in any well‑founded interpretation.   
      
   --   
   Copyright 2026 Olcott

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

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