XPost: comp.theory, sci.math   
   From: mikko.levanto@iki.fi   
      
   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.   
      
   --   
   Mikko   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)