XPost: comp.theory, sci.math   
   From: polcott333@gmail.com   
      
   On 2/19/2026 4:06 AM, Mikko wrote:   
   > On 18/02/2026 21:48, polcott wrote:   
   >> On 2/18/2026 3:10 AM, Mikko wrote:   
   >>> On 17/02/2026 14:59, polcott wrote:   
   >>>> On 2/17/2026 3:03 AM, Mikko wrote:   
   >>>>> On 16/02/2026 15:47, olcott wrote:   
   >>>>>> On 2/16/2026 5:25 AM, Mikko wrote:   
   >>>>>>> On 15/02/2026 15:02, polcott wrote:   
   >>>>>>>> ∀x ∈ PA (True(PA, x) ↔ PA ⊢ x)   
   >>>>>>>> Does not mean to test every x in PA   
   >>>>>>>   
   >>>>>>> No, it merely declares that there are two symbols for one predicate   
   >>>>>>> (which, if interpreted accordint to the usual meaning of either   
   >>>>>>> symbol,   
   >>>>>>> is uncomputable).   
   >>>>>>   
   >>>>>> What do you think that this means: PA ⊢ x ?   
   >>>>>   
   >>>>> The exact meaning depends on the context and the meanings of the   
   >>>>> types of the left and right side expressions. The usual metalogical   
   >>>>> meaning   
   >>>>> is that x is a theorem of some variant of PA. If something else is   
   >>>>> meant that should be specified in the opus where the expression is   
   >>>>> used   
   >>>>   
   >>>> Yes that is correct. What does that mean?   
   >>>   
   >>> It means that the author must define the symbols in the opus they are   
   >>> used.   
   >>   
   >> Is this your best answer or are you trying to be evasive?   
   >   
   > Whether another answer would be better is a matter of taste, at least   
   > to some extent.   
   >   
      
   PA ⊢ x   
   The correct answer is   
   A back-chained inference from x to the axioms of PA exists   
      
   --   
   Copyright 2026 Olcott   
      
   My 28 year goal has been to make   
   "true on the basis of meaning expressed in language"   
   reliably computable for the entire body of knowledge.   
      
   This required establishing a new foundation   
   for correct reasoning.   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)