XPost: sci.logic, comp.theory, sci.math   
   From: mikko.levanto@iki.fi   
      
   olcott kirjoitti 29.11.2025 klo 19.54:   
   > On 11/29/2025 4:17 AM, Mikko wrote:   
   >> olcott kirjoitti 28.11.2025 klo 17.51:   
   >>> On 11/28/2025 2:58 AM, Mikko wrote:   
   >>>> 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.   
   >>>   
   >>> ∀x ∈ Human (Bachelor(x) ↔ (Male(x) ∧ Adult(x) ∧ ~Married(x)))   
   >>   
   >> That is a different sentence. The syntax rules of   
   >>      https://philarchive.org/archive/PETMTT-4v2   
   >> are different for := and =.   
   >   
   > It is equivalent. The term Bachelor(x) is still defined by   
   > Male(x) ∧ Adult(x) ∧ ~Married(x) ∧ Human(x) thus never   
   > circular at all as Willard Van Orman Quine insisted.   
      
   It is not equivalent. The one with ↔ merely claims it without saying   
   why that is claimed. It may be a consequence of earlier assumtions   
   or a new assumtion or a part of a quesstion. It cannot be a definition   
   or a consequence of earlier definitions because MTT does not permit a   
   definition of Bachelor, Male, Adult, or Married, or any other predicate.   
      
   --   
   Mikko   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)