XPost: comp.theory, sci.math, comp.lang.prolog   
   From: polcott333@gmail.com   
      
   On 12/10/2025 4:04 AM, Mikko wrote:   
   > olcott kirjoitti 8.12.2025 klo 21.09:   
   >> On 12/8/2025 3:13 AM, Mikko wrote:   
   >>> olcott kirjoitti 5.12.2025 klo 19.43:   
   >>>> On 12/5/2025 3:38 AM, Mikko wrote:   
   >>>>> olcott kirjoitti 4.12.2025 klo 16.06:   
   >>>>>> On 12/4/2025 2:58 AM, Mikko wrote:   
   >>>>>>> Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:   
   >>>>>>>> On 30/11/2025 09:58, Mikko wrote:   
   >>>>>>>>   
   >>>>>>>>> Note that the meanings of   
   >>>>>>>>>   ?- G = not(provable(F, G)).   
   >>>>>>>>> and   
   >>>>>>>>>   ?- unify_with_occurs_check(G, not(provable(F, G))).   
   >>>>>>>>> are different. The former assigns a value to G, the latter does   
   >>>>>>>>> not.   
   >>>>>>>   
   >>>>>>>> For sufficiently informal definitions of "value".   
   >>>>>>>> And for sufficiently wrong ones too!   
   >>>>>>>   
   >>>>>>> It is sufficiently clear what "value" of a Prolog variable means.   
   >>>>>   
   >>>>>> % This sentence cannot be proven in F   
   >>>>>> ?- G = not(provable(F, G)).   
   >>>>>> G = not(provable(F, G)).   
   >>>>>> ?- unify_with_occurs_check(G, not(provable(F, G))).   
   >>>>>> false.   
   >>>>>>   
   >>>>>> I would say that the above Prolog is the 100%   
   >>>>>> complete formal specification of:   
   >>>>>>   
   >>>>>> "This sentence cannot be proven in F"   
   >>>>>   
   >>>>> The first query can be regarded as a question whether "G =   
   >>>>> not(provable(   
   >>>>> F, G))" can be proven for some F and some G. The answer is that it can   
   >>>>> for every F and for (at least) one G, which is not(provable(G)).   
   >>>>>   
   >>>>> The second query can be regarded as a question whether "G =   
   >>>>> not(provable   
   >>>>> (F, G))" can be proven for some F and some G that do not contain   
   >>>>> cycles.   
   >>>>> The answer is that in the proof system of Prolog it cannot be.   
   >>>>   
   >>>> No that it flatly incorrect. The second question is this:   
   >>>> Is "G = not(provable(F, G))." semantically sound?   
   >>>   
   >>> Where is the definition of Prolog semantics is that said?   
   >>   
   >> Any expression of Prolog that cannot be evaluated to   
   >> a truth value because it specifies non-terminating   
   >> infinite recursion is "semantically unsound" by the   
   >> definition of those terms even if Prolog only specifies   
   >> that cannot be evaluated to a truth value because it   
   >> specifies non-terminating infinite recursion.   
   >   
   > Your Prolog implementation has evaluated G = not(provablel(F, G))   
   > to a truth value true. When doing so it evaluated each side of =   
   > to a value that is not a truth value.   
   >   
      
   ?- unify_with_occurs_check(G, not(provable(F, G))).   
   false.   
      
   Proves that   
   G = not(provable(F, G)).   
   would remain stuck in infinite recursion.   
      
   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.   
      
   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.   
      
   Note that, whereas they may allow you to construct something   
   like this, most Prolog systems will not be able to write it   
   out at the end. According to the formal definition of   
   Unification, this kind of “infinite term” should never come   
   to exist. Thus Prolog systems that allow a term to match an   
   uninstantiated subterm of itself do not act correctly as   
   Resolution theorem provers. In order to make them do so, we   
   would have to add a check that a variable cannot be   
   instantiated to something containing itself. Such a check,   
   an occurs check, would be straightforward to implement, but   
   would slow down the execution of Prolog programs considerably.   
   Since it would only affect very few programs, most implementors   
   have simply left it out 1.   
      
   1 The Prolog standard states that the result is undefined if   
   a Prolog system attempts to match a term against an uninstantiated   
   subterm of itself, which means that programs which cause this to   
   happen will not be portable. A portable program should ensure that   
   wherever an occurs check might be applicable the built-in predicate   
   unify_with_occurs_check/2 is used explicitly instead of the normal   
   unification operation of the Prolog implementation. As its name   
   suggests, this predicate acts like =/2 except that it fails if an   
   occurs check detects an illegal attempt to instantiate a variable.   
   END:(Clocksin & Mellish 2003:254)   
      
   Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog   
   Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg:   
   Springer-Verlag.   
      
      
   --   
   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)