XPost: comp.theory, sci.math   
   From: polcott333@gmail.com   
      
   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?   
      
   --   
   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)