XPost: sci.math, comp.theory   
   From: polcott333@gmail.com   
      
   On 1/27/2026 2:15 AM, Mikko wrote:   
   > On 26/01/2026 18:45, Richard Damon wrote:   
   >> On 1/26/26 10:22 AM, olcott wrote:   
   >>> On 1/26/2026 6:55 AM, Mikko wrote:   
   >>>> On 25/01/2026 15:30, olcott wrote:   
   >>>>> On 1/25/2026 5:24 AM, Mikko wrote:   
   >>>>>> On 24/01/2026 16:18, olcott wrote:   
   >>>>>>> On 1/24/2026 2:23 AM, Mikko wrote:   
   >>>>>>>> On 22/01/2026 18:47, olcott wrote:   
   >>>>>>>>> On 1/22/2026 2:21 AM, Mikko wrote:   
   >>>>>>>>   
   >>>>>>>>>> Anyway, what can be provven that way is true aboout PA. You   
   >>>>>>>>>> can deny   
   >>>>>>>>>> the proof but you cannot perform what is meta-provably   
   >>>>>>>>>> impossible.   
   >>>>>>>>   
   >>>>>>>>> The meta-proof does not exist in the axioms of PA   
   >>>>>>>>> and that is the reason why an external truth in   
   >>>>>>>>> an external model cannot be proved internally in PA.   
   >>>>>>>>> All of these years it was only a mere conflation   
   >>>>>>>>> error.   
   >>>>>>>>   
   >>>>>>>> It is perfectly clear which is which. But every proof in PA is also   
   >>>>>>>> a proof in Gödel's metatheory.   
   >>>>>>>   
   >>>>>>> ∀x ∈ PA (  True(PA, x) ≡ PA ⊢  x )   
   >>>>>>> ∀x ∈ PA ( False(PA, x) ≡ PA ⊢ ¬x )   
   >>>>>>> ∀x ∈ PA ( ¬WellFounded(PA, x) ≡   
   >>>>>>>           (¬True(PA, x) ∧ (¬False(PA, x)))   
   >>>>>>   
   >>>>>> Those sentences don't mean anything without specificantions of a   
   >>>>>> language and a theory that gives them some meaning.   
   >>>>>   
   >>>>> In other word you do not understand standard notational   
   >>>>> conventions that define True for PA as provable from the   
   >>>>> axioms of PA and False for PA as refutable from the axioms   
   >>>>> of PA.   
   >>>>   
   >>>> There are no notational convention that defines True, False, and   
   >>>> WellFounded with two arguments. And you did not specify in which   
   >>>> context your sentences are true or otherwise relevant.   
   >>>>   
   >>>   
   >>> “x is a single finite string representing   
   >>> a PA‑formula, such as ‘2 + 3 = 5’.   
   >>> True(PA, x), False(PA, x), and WellFounded(PA, x)   
   >>> are meta‑level unary predicates classifying   
   >>> that formula by its provability in PA.”   
   >>   
   >> In outher words, you ACCEPT that the meta level can define what is   
   >> true in PA?   
   >   
      
   A meta level is even required to prove what is true   
   in actual PA. This meta-level does a back-chained   
   inference from x to the axioms of PA.   
      
   > In the metatheory one can construct a model of PA. Everyting in that   
   > model can be proven in the metatheory is true in that model so it is   
   > true in some model of PA.   
   >   
      
   Yes I am making sure to exclude that. Confusion between   
   what is actually true in actual PA and what is true in   
   separate models of arithmetic is how the misconception   
   of incompleteness arose.   
      
   >> I thought you said that PA had to be able to determine the truth itself?   
   >   
      
   PA doesn't even have a provability operator so we need   
   a meta-level for that. Unlike how it is conventionally   
   done I exclude the standard model of arithmetic completely.   
      
   Any expression not derivable from the axioms of PA is   
   non-well-founded in PA. The misconception of incompleteness   
   only arose because true in PA was incorrectly conflated   
   with true in the standard model of arithmetic.   
      
   > No, I said it doesn't. But what is provable in first order PA is true in   
   > every model of first order PA and what is not provable in PA is false in   
   > some model of first order PA. But there is no known way to extend this   
   > result to the second order, and the original PA is a sencond order   
   > theory.   
   >   
      
      
   --   
   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)