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