XPost: comp.theory, sci.math   
   From: polcott333@gmail.com   
      
   On 2/19/2026 8:44 PM, Richard Damon wrote:   
   > On 2/19/26 6:47 AM, 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   
   >>   
   >   
   > No, that is *ONE* definition of it, but in other contexts, it might mean   
   > something different.   
   >   
   > All you are doing is proving you don't understand the importance of   
   > context for definitions.   
   >   
   > In fact, I rarely hear about it specifing that a "back chain" exists,   
   > instead it normally is described as there exists a "proof" of x in PA.   
   >   
   > Proofs, are more normally talked about as something that moves in the   
   > FORWARD direction, from the axioms of the system to the conclusion, not   
   > about "back-chaining".   
   >   
   >   
      
   That is correct   
      
   --   
   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
   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)