XPost: comp.theory, sci.math, comp.lang.prolog   
   From: mikko.levanto@iki.fi   
      
   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?   
      
   When "G = not(provable(F, G))." is used as a Prolog goal the   
   applied semantics is what Prolog lauguage definition specifies.   
   Does "semantically sound" mean something in that context?   
      
   At least your Prolog interpretation finds it meaningful. It determines   
   that the excution of that goal succeeds and assigns a value G but not   
   to F.   
      
   --   
   Mikko   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)