XPost: sci.logic, comp.theory, sci.math   
   From: mikko.levanto@iki.fi   
      
   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. For properies and relation the   
   alternative would be that a predicate is false if any of the arguments   
   are of wrong type. For functions it is harder to find a reasonable value   
   if an argument is of wrong type.   
      
   This is of course irrelevant to the point that the resulting theory is   
   not formal unless both the definition of semantics and the definition of   
   semantic logical entailment are fully formal.   
      
   --   
   Mikko   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)