XPost: comp.theory, sci.math, sci.lang   
   From: polcott333@gmail.com   
      
   On 12/1/2025 5:02 AM, Mikko wrote:   
   > olcott kirjoitti 29.11.2025 klo 23.59:   
   >   
   > G := (F ⊬ G) // G says of itself that it is unprovable in F   
   >   
   > With a reasonable type system that is a type error:   
   > - the symbol ⊬ requires a sentence on the right side   
   > - the value of the ⊬ operation is a truth value   
   > - the symbol := requires the same type on both sides   
   > - thus G must be both a sentence and a truth value   
   >   
   > But G cannot be both. A sentence has a truth value but it isn't one.   
   >   
      
   % 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.   
      
   It is an expression of language having no truth value   
   because it is not a logic sentence.   
      
   https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)   
      
   --   
   Copyright 2025 Olcott   
      
   My 28 year goal has been to make   
   "true on the basis of meaning" computable.   
      
   This required establishing a new foundation   
   for correct reasoning.   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)