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