XPost: comp.theory, sci.math, comp.prolog   
   From: mikko.levanto@iki.fi   
      
   olcott kirjoitti 11.12.2025 klo 16.15:   
   > On 12/11/2025 2:40 AM, Mikko wrote:   
   >> olcott kirjoitti 10.12.2025 klo 18.29:   
   >>> On 12/10/2025 4:10 AM, Mikko wrote:   
   >>>> olcott kirjoitti 8.12.2025 klo 21.12:   
   >>>>> On 12/5/2025 4:49 AM, Tristan Wibberley wrote:   
   >>>>>> On 04/12/2025 14:06, olcott wrote:   
   >>>>>>   
   >>>>>>> % 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.   
   >>>>>>>   
   >>>>>>> I would say that the above Prolog is the 100%   
   >>>>>>> complete formal specification of:   
   >>>>>>>   
   >>>>>>> "This sentence cannot be proven in F"   
   >>>>>>   
   >>>>>> No. I think I showed in one of my recent posts (using definition   
   >>>>>> extensions) that you need to formalise the mathematicians notion of   
   >>>>>> "proof /in/ [system]" vis-a-vis "let" and its stronger sibling   
   >>>>>> "suppose". That's a bigger job than you've done.   
   >>>>>>   
   >>>>>> I need a new quotation convention for referring to things whose   
   >>>>>> name has   
   >>>>>> an existing meaning in my U-language, I quoted "let" and "suppose"   
   >>>>>> as if   
   >>>>>> I were using their names; I mean to use the things themselves, but   
   >>>>>> they   
   >>>>>> have to be quoted in some way to distinguish the objects of   
   >>>>>> mathematical   
   >>>>>> language from the verbs of ordinary language without introducing such   
   >>>>>> incidental new names as I would otherwise need.   
   >>>>   
   >>>>> Semantics tautologies that define finite strings in   
   >>>>> terms of other finite strings to give the LHS its   
   >>>>> semantic meaning on the basis of the RHS.   
   >>>>   
   >>>> You havn't given a single example of a smenatic tautology that can be   
   >>>> interpreted as a definition nor a single example of defintion that is   
   >>>> a semantic tautology. Perhaps it is possible if you define "semantic   
   >>>> taultology" so that it needn't be anything like a tautology.   
   >>>   
   >>>  From my signature line:   
   >>> "true on the basis of meaning expressed in language"   
   >>>   
   >>> Here is an example: "cats"  "animals"   
   >>   
   >> Yes, that is an example of your inability mentioned above.   
   >>   
   >> Your example not define anything and therefore is neither an exmaple   
   >> of a semantic tautology that can be interpreted as a defintion nor an   
   >> axample of a defintion that is a semantic tautology.   
   >   
   > 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.   
   >   
   > The finite string "cats" is stipulated to have   
   > the type_of_relation  to the finite string   
   > "animals".   
      
   Perhaps, but any definition of "cat" must exlude some animals as   
   non-cats. Yor above example of semantic tautology doesn't do that.   
      
   Note that the meaning of "cat" varies from 'Felis catus L.' to 'Felidae   
   Fischer von Waldheim 1817' and even to non-animals.   
      
   --   
   Mikko   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)