Forums before death by AOL, social media and spammers... "We can't have nice things"
| sci.logic | Logic -- math, philosophy & computationa | 262,912 messages |
[ << oldest | < older | list | newer > | newest >> ]
| Message 262,767 of 262,912 |
| olcott to Mikko |
| Re: The Halting Problem asks for too muc |
| 31 Jan 26 09:23:51 |
XPost: comp.theory, sci.math From: polcott333@gmail.com On 1/31/2026 2:41 AM, Mikko wrote: > On 30/01/2026 16:35, olcott wrote: >> On 1/30/2026 3:34 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. >>> >>> That would have no effet. Even if the metalanguage had an occcurs_check >>> it would not be necessary to use it in a proof. >> >> It would only seem to have no effect because you >> never bothered to understand what an occurs_check is. > > That assumption is false. > So far you have conclusively proven that you do not understand what an occurs_check is. If you want to provide that you do know then you must provide all of the correct details. Merely claiming that my statement is false is an assertion entirely bereft of supporting reasoning thus inherently baseless. >> Truth is computable because “meaningful sentence” >> is defined as “sentence with a well-founded >> justification tree,” and evaluating any well-founded >> tree always terminates. Anything else isn’t truth-apt. > > That "bcause" is wrong. Whether a sentence has a well-founded > justifiation tree is not computable, especially for arithmetic > sentences. > My one half page of text explaining all of the key details of my 28 years of work was completely validated by five different LLM systems. proof theoretic semantics is correct model theoretic semantics is profoundly wrong-headed. Your ignorance of the details of well-founded proof theoretic semantics makes your rebuttal baseless. > But that does not alter the fact that an existence or non-existence > of a metalanguage feature that is not present in the justification > tree is irrelevant. > An existence or non-existence of a metalanguage feature is entirely anchored in a totally wrong-headed notion. The only way that this can be seen is to become an expert in well-founded proof theoretic semantics. -- Copyright 2026 Olcott |
(c) 1994, bbs@darkrealms.ca