XPost: comp.theory, sci.math   
   From: mikko.levanto@iki.fi   
      
   On 19/02/2026 13:47, polcott wrote:   
   > 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   
      
   As I already said, the usual meaning is that the inferences must   
   syntactically valid as required by the rules of PA.   
      
   --   
   Mikko   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)