XPost: sci.math, comp.theory   
   From: polcott333@gmail.com   
      
   On 12/10/2025 9:01 AM, Python wrote:   
   > Le 10/12/2025 à 15:11, olcott a écrit :   
   > ..   
   >> unify_with_occurs_check() examines the directed   
   >> graph of the evaluation sequence of an expression.   
   >> When it detects a cycle that indicates that an   
   >> expression would remain stuck in recursive   
   >> evaluation never to be resolved to a truth value.   
   >   
   >   
   > unify_with_occurs_check(G, not(provable(F, G))). returning false does   
   > NOT prove that   
   > G = not(provable(F, G)) “gets stuck in infinite recursion.”   
   >   
   > All it proves is this:   
   >   
   > With finite Prolog terms, you cannot unify a variable with a structure   
   > that contains that same variable — the occurs-check rejects cyclic self-   
   > reference.   
   >   
      
   cycle means cycle in the directed graph as shown below.   
      
   > So the failure of unification means only:   
   >   
   > Prolog refuses to build an illegal self-referential term,   
   >   
   > not that the logical statement or predicate would “infinitely recurse.”   
   >   
      
      "Prolog implementations usually omit the occurs   
      check for reasons of efficiency, which can lead   
      to circular data structures and looping."   
   as shown in the image of the directed graph with a cycle   
      
   https://en.wikipedia.org/wiki/Occurs_check#Rational_tree_unification   
      
   The reason why I know these deeper details is that I   
   created Olcott's Minimal Type Theory to translate   
   formal expressions into the directed graph of their   
   evaluation sequence.   
      
   > This is the usual Olcott confusion:   
   > he mistakes a language-specific operational failure (Prolog term   
   > construction) for a deep theorem about provability or self-reference.   
   >   
   > Gödel diagonalization never uses this kind of naive unification, so the   
   > Prolog failure is irrelevant to logic.   
      
      
      
   --   
   Copyright 2025 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)