XPost: comp.theory, sci.math, comp.prolog   
   From: polcott333@gmail.com   
      
   On 12/5/2025 4:49 AM, Tristan Wibberley wrote:   
   > On 04/12/2025 14:06, olcott wrote:   
   >   
   >> % 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"   
   >   
   > No. I think I showed in one of my recent posts (using definition   
   > extensions) that you need to formalise the mathematicians notion of   
   > "proof /in/ [system]" vis-a-vis "let" and its stronger sibling   
   > "suppose". That's a bigger job than you've done.   
   >   
   > I need a new quotation convention for referring to things whose name has   
   > an existing meaning in my U-language, I quoted "let" and "suppose" as if   
   > I were using their names; I mean to use the things themselves, but they   
   > have to be quoted in some way to distinguish the objects of mathematical   
   > language from the verbs of ordinary language without introducing such   
   > incidental new names as I would otherwise need.   
   >   
      
   Semantics tautologies that define finite strings in   
   terms of other finite strings to give the LHS its   
   semantic meaning on the basis of the RHS.   
      
   --   
   Copyright 2025 Olcott

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

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