XPost: comp.theory, sci.math, sci.lang   
   From: mikko.levanto@iki.fi   
      
   olcott kirjoitti 2.12.2025 klo 16.00:   
   > On 12/2/2025 2:53 AM, Mikko wrote:   
   >> olcott kirjoitti 1.12.2025 klo 19.15:   
   >>> 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)   
   >>   
   >> Yes, that is the exxential difference between the two G's.   
   >> The expession F ⊬ G has a truth value because it is either   
   >> true or false   
   >   
   > I propose that is a false assumption.   
      
   If you want to propose anygthng like that you should   
   (a) specify what is the assumption you want to propose as false   
   (b) why should that assumption be considered false   
   (c) what assumption would be true or at least less obviously false   
      
   --   
   Mikko   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)