XPost: comp.theory, sci.math, sci.lang   
   From: mikko.levanto@iki.fi   
      
   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.   
      
   --   
   Mikko   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)