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