XPost: comp.theory, sci.math   
   From: mikko.levanto@iki.fi   
      
   On 31/01/2026 17:26, olcott wrote:   
   > On 1/31/2026 2:56 AM, Mikko wrote:   
   >> On 29/01/2026 15:57, olcott wrote:   
   >>> On 1/29/2026 3:12 AM, Mikko wrote:   
   >>>> On 28/01/2026 15:49, olcott wrote:   
   >>>>> On 1/28/2026 3:54 AM, Mikko wrote:   
   >>>>>> On 27/01/2026 17:32, olcott wrote:   
   >>>>>>> On 1/27/2026 2:17 AM, Mikko wrote:   
   >>>>>>>> On 26/01/2026 18:58, olcott wrote:   
   >>>>>>>>> On 1/26/2026 10:45 AM, 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?   
   >>>>>>>>>>   
   >>>>>>>>>> I thought you said that PA had to be able to determine the   
   >>>>>>>>>> truth itself?   
   >>>>>>>>>   
   >>>>>>>>> We need a meta-level truth predicate anchored   
   >>>>>>>>> only in the axioms of PA itself and thus not   
   >>>>>>>>> anchored in the standard model of arithmetic.   
   >>>>>>>>   
   >>>>>>>> That predicate is not computable.   
   >>>>>>>   
   >>>>>>> That was Tarski's mistake.   
   >>>>>>   
   >>>>>> No, Tarski's proof is about a different problem, though the results   
   >>>>>> are related and there are much similarity in the proofs. Tarski did   
   >>>>>> not use Turing machines in the proof but a computability proof must   
   >>>>>> use that.   
   >>>>>   
   >>>>> Because you refuse to understand the underlying   
   >>>>> details of what occurs_check means I cannot   
   >>>>> explain to you how Tarski erred.   
   >>>>   
   >>>> Irrelevant. There is no "occurs_check" in Tarski's proof.   
   >>>>   
   >>>   
   >>> If there was then there never would be a Tarski proof.   
   >>> https://liarparadox.org/Tarski_247_248.pdf   
   >>   
   >> Irrelevant. Tarski's proof is what it is and there is no "occurs_check"   
   >> there.   
      
   > Sure and a car that has a missing engine will always   
   > be a car that will not run.   
      
   That's true, too.   
      
   --   
   Mikko   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)