XPost: comp.theory, sci.math, comp.ai.philosophy   
   From: mikko.levanto@iki.fi   
      
   olcott kirjoitti 27.11.2025 klo 17.31:   
   > On 11/27/2025 1:56 AM, Mikko wrote:   
   >> olcott kirjoitti 26.11.2025 klo 17.39:   
   >>> 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. 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.   
   >>>   
   >>> The body of knowledge is defined in terms of Rudolf Carnap Meaning   
   >>> Postulates and stored in a knowledge ontology inheritance hierarchy.   
   >>>   
   >>> The predicate Bachelor(x) is stipulated to mean ~Married(x) where the   
   >>> predicate Married(x) is defined in terms of billions of other things   
   >>> such as all of the details of Human(x).   
   >>   
   >> That, too, is 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.   
      
   > In Olcott's Minimal Type Theory Rudolf Carnap Meaning   
   > Postulates directly encode semantic meaning in the syntax.   
      
   if the encoding is not fully formally specified the theory is not   
   formal.   
      
   > The meaningless finite string "Bachelor" is defined as   
   > a semantic predicate through other already defined terms   
   > ∀x (Bachelor(x) := (Male(x) ∧ Human(x) ∧ ~Married(x)))   
   > Adapted by Olcott from Rudolf Carnap Meaning postulates.   
   >   
   > And encoded in the syntax of Olcott's Minimal Type Theory   
   > https://philarchive.org/archive/PETMTT-4v2   
      
   That page only tells how to define a sentence in terms of other   
   sentences. As it does not permit any arguments on the left side of :=   
   the expression ∀x (Bachelor(x) := (Male(x) ∧ Human(x) ∧ ~Married(x)))   
   is syntactically invalid.   
      
   --   
   Mikko   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)