XPost: comp.theory, sci.math, sci.lang   
   From: polcott333@gmail.com   
      
   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.   
   G := (F ⊬ G) expands to   
   (F ⊬ (F ⊬ (F ⊬ (F ⊬ (F ⊬ (F ⊬ ...))))))   
      
   and Prolog agrees G = not(provable(F, G)).   
   expands to: not(provable(F, not(provable(F, not(provable(F, ...))))))   
      
   We completely bypass all of this by creating a formal   
   language that fully integrates semantics directly in   
   the syntax. In this case not provable in F simply means   
   not true in F.   
      
   Truthmaker Maximalism is an entire field of philosophy   
   that deals with this.   
      
   We can implement the notion of a Tarski theory / meta-theory   
   in a single formal language implementing Gödel's 1944   
   "theory of simple types".   
      
   "This sentence is not true" has a semantic type of   
   ~truth_bearer. That is what makes this sentence true:   
   This sentence is not true: "This sentence is not true"   
      
   > that G is no provable in F, and the same truth   
   > value is given to G in the expression G := (F ⊬ G). The   
   > Prolog term not(provable(F, G)) does not have a truth value.   
      
   Yes you are getting it now.   
      
   > After G = not(provable(F, G)) the value of G is that data   
   > structure, so it has no truth value, unlike the G in   
   > G := (F ⊬ G).   
   >   
      
   Maybe we should stick with the Prolog then. I only   
   created Minimal Type Theory because I didn't know   
   that Prolog could to the same thing.   
      
   Because I created Minimal Type Theory I know that   
   pathological self-reference(Olcott 2004) creates   
   cycles in the directed graph of evaluation sequence   
   thus showing that evaluation gets stuck in an infinite   
   loop never reaching a truth value.   
      
   --   
   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)