XPost: sci.logic, comp.theory, sci.math   
   From: mikko.levanto@iki.fi   
      
   olcott kirjoitti 29.11.2025 klo 19.57:   
   > On 11/29/2025 4:20 AM, Mikko wrote:   
   >> olcott kirjoitti 28.11.2025 klo 17.54:   
   >>> On 11/28/2025 3:01 AM, Mikko wrote:   
   >>>> olcott kirjoitti 27.11.2025 klo 17.43:   
   >>>>> On 11/27/2025 2:00 AM, Mikko wrote:   
   >>>>>> olcott kirjoitti 26.11.2025 klo 17.54:   
   >>>>>>> On 11/26/2025 5:37 AM, Mikko wrote:   
   >>>>>>>> olcott kirjoitti 25.11.2025 klo 16.21:   
   >>>>>>>>> On 11/25/2025 3:40 AM, Mikko wrote:   
   >>>>>>>>>> olcott kirjoitti 25.11.2025 klo 2.53:   
   >>>>>>>>>>> Eliminating undecidability and mathematical incompleteness   
   >>>>>>>>>>> merely requires discarding model theory and fully integrating   
   >>>>>>>>>>> semantics directly into the syntax of the formal language.   
   >>>>>>>>>>>   
   >>>>>>>>>>> The only inference step allowed is semantic logical   
   >>>>>>>>>>> entailment and this is performed syntactically. A formal   
   >>>>>>>>>>> language such as Montague Grammar or CycL of the Cyc   
   >>>>>>>>>>> project can encode the semantics of anything that can   
   >>>>>>>>>>> be expressed in language.   
   >>>>>>>>>>   
   >>>>>>>>>> The resulting theory is not formal unless both the definition of   
   >>>>>>>>>> semantics and the definition of semantic logical entailment are   
   >>>>>>>>>> fully formal.   
   >>>>>>>>>>   
   >>>>>>>>>>   
   >>>>>>>>>   
   >>>>>>>>> https://plato.stanford.edu/entries/montague-semantics/   
   >>>>>>>>> https://en.wikipedia.org/wiki/CycL   
   >>>>>>>>> https://en.wikipedia.org/wiki/Ontology_(information_science)   
   >>>>>>>>>   
   >>>>>>>>> *This was my original inspiration*   
   >>>>>>>>> Kurt Gödel in his 1944 Russell's mathematical logic gave the   
   >>>>>>>>> following definition of the "theory of simple types" in a   
   >>>>>>>>> footnote:   
   >>>>>>>>>   
   >>>>>>>>> By the theory of simple types I mean the doctrine which says   
   >>>>>>>>> that the objects of thought (or, in another interpretation, the   
   >>>>>>>>> symbolic expressions) are divided into types, namely:   
   >>>>>>>>> individuals, properties of individuals, relations between   
   >>>>>>>>> individuals, properties of such relations, etc. (with a similar   
   >>>>>>>>> hierarchy for extensions), and that sentences of the form: " a   
   >>>>>>>>> has the property φ ", " b bears the relation R to c ", etc. are   
   >>>>>>>>> meaningless, if a, b, c, R, φ are not of types fitting together.   
   >>>>>>>>   
   >>>>>>>> That is a constraint on the language. Note that individuals of   
   >>>>>>>> all sorts   
   >>>>>>>> are considered to be of the same type.   
   >>>>>>>   
   >>>>>>> An individual house, person, orange, piece of pie,   
   >>>>>>> is not a group of houses, people, oranges, pieces of pie.   
   >>>>>>   
   >>>>>> In the type system Gödel called minimal all of those would be   
   >>>>>> individuals and therefore of the same type.   
   >>>>   
   >>>>> Then Gödel would be wrong.   
   >>>>   
   >>>> No, what he said was perfectly true about what the words meant   
   >>>> at the time. Your preferences may differ but there is no right   
   >>>> or wrong in matters of taste.   
   >>>   
   >>> There is a correct mapping of finite strings   
   >>> to the semantic meaning that they specify.   
   >>   
   >> Yes, amd accoprding to that mapping what Gödel said is true.   
   >>   
   >   
   > % 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.   
   >   
   > ...We are therefore confronted with a proposition which asserts its own   
   > unprovability. 15 … (Gödel 1931:40-41)   
   >   
   > That thereby makes itself semantically unsound.   
      
   No, everything above has a meaning and it is not hard to work out what   
   that meaning is. Note that the meanings of   
     ?- G = not(provable(F, G)).   
   and   
     ?- unify_with_occurs_check(G, not(provable(F, G))).   
   are different. The former assigns a value to G, the latter does not.   
      
   --   
   Mikko   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)