XPost: sci.logic, sci.math, comp.theory   
   From: mikko.levanto@iki.fi   
      
   On 18/01/2026 15:28, olcott wrote:   
   > On 1/18/2026 5:27 AM, Mikko wrote:   
   >> On 17/01/2026 16:47, olcott wrote:   
   >>> On 1/17/2026 3:53 AM, Mikko wrote:   
   >>>> On 16/01/2026 17:38, olcott wrote:   
   >>>>> On 1/16/2026 3:32 AM, Mikko wrote:   
   >>>>>> On 15/01/2026 22:30, olcott wrote:   
   >>>>>>> On 1/15/2026 3:34 AM, Mikko wrote:   
   >>>>>>>> On 14/01/2026 21:32, olcott wrote:   
   >>>>>>>>> On 1/14/2026 3:01 AM, Mikko wrote:   
   >>>>>>>>>> On 13/01/2026 16:31, olcott wrote:   
   >>>>>>>>>>> On 1/13/2026 3:13 AM, Mikko wrote:   
   >>>>>>>>>>>> On 12/01/2026 16:32, olcott wrote:   
   >>>>>>>>>>>>> On 1/12/2026 4:47 AM, Mikko wrote:   
   >>>>>>>>>>>>>> On 11/01/2026 16:24, Tristan Wibberley wrote:   
   >>>>>>>>>>>>>>> On 11/01/2026 10:13, Mikko wrote:   
   >>>>>>>>>>>>>>>> On 10/01/2026 17:47, olcott wrote:   
   >>>>>>>>>>>>>>>>> On 1/10/2026 2:23 AM, Mikko wrote:   
   >>>>>>>>>>>>>>>   
   >>>>>>>>>>>>>>>>>> No, that does not follow. If a required result cannot   
   >>>>>>>>>>>>>>>>>> be derived by   
   >>>>>>>>>>>>>>>>>> appying a finite string transformation then the it it   
   >>>>>>>>>>>>>>>>>> is uncomputable.   
   >>>>>>>>>>>>>>>>>   
   >>>>>>>>>>>>>>>>> Right. Outside the scope of computation. Requiring   
   >>>>>>>>>>>>>>>>> anything   
   >>>>>>>>>>>>>>>>> outside the scope of computation is an incorrect   
   >>>>>>>>>>>>>>>>> requirement.   
   >>>>>>>>>>>>>>>>   
   >>>>>>>>>>>>>>>> You can't determine whether the required result is   
   >>>>>>>>>>>>>>>> computable before   
   >>>>>>>>>>>>>>>> you have the requirement.   
   >>>>>>>>>>>>>>>   
   >>>>>>>>>>>>>>>   
   >>>>>>>>>>>>>>> Right, it is /in/ scope for computer science... for the /   
   >>>>>>>>>>>>>>> ology/. Olcott   
   >>>>>>>>>>>>>>> here uses "computation" to refer to the practice. You   
   >>>>>>>>>>>>>>> give the   
   >>>>>>>>>>>>>>> requirement to the /ologist/ who correctly decides that   
   >>>>>>>>>>>>>>> it is not for   
   >>>>>>>>>>>>>>> computation because it is not computable.   
   >>>>>>>>>>>>>>>   
   >>>>>>>>>>>>>>> You two so often violently agree; I find it warming to   
   >>>>>>>>>>>>>>> the heart.   
   >>>>>>>>>>>>>>   
   >>>>>>>>>>>>>> For pracitcal programming it is useful to know what is   
   >>>>>>>>>>>>>> known to be   
   >>>>>>>>>>>>>> uncomputable in order to avoid wasting time in attemlpts   
   >>>>>>>>>>>>>> to do the   
   >>>>>>>>>>>>>> impossible.   
   >>>>>>>>>>>>>   
   >>>>>>>>>>>>> It f-cking nuts that after more than 2000 years   
   >>>>>>>>>>>>> people still don't understand that self-contradictory   
   >>>>>>>>>>>>> expressions: "This sentence is not true" have no   
   >>>>>>>>>>>>> truth value. A smart high school student should have   
   >>>>>>>>>>>>> figured this out 2000 years ago.   
   >>>>>>>>>>>>   
   >>>>>>>>>>>> Irrelevant. For practical programming that question needn't   
   >>>>>>>>>>>> be answered.   
   >>>>>>>>>>>   
   >>>>>>>>>>> The halting problem counter-example input is anchored   
   >>>>>>>>>>> in the Liar Paradox. Proof Theoretic Semantics rejects   
   >>>>>>>>>>> those two and Gödel's incompleteness and a bunch more   
   >>>>>>>>>>> as merely non-well-founded inputs.   
   >>>>>>>>>>   
   >>>>>>>>>> For every Turing machine the halting problem counter-example   
   >>>>>>>>>> provably   
   >>>>>>>>>> exists.   
   >>>>>>>>>   
   >>>>>>>>> Not when using Proof Theoretic Semantics grounded   
   >>>>>>>>> in the specification language. In this case the   
   >>>>>>>>> pathological input is simply rejected as ungrounded.   
   >>>>>>>>   
   >>>>>>>> Then your "Proof Theoretic Semantics" is not useful for   
   >>>>>>>> discussion of   
   >>>>>>>> Turing machines. For every Turing machine a counter example exists.   
   >>>>>>>> And so exists a Turing machine that writes the counter example when   
   >>>>>>>> given a Turing machine as input.   
   >>>>>>>   
   >>>>>>> It is "not useful" in the same way that ZFC was   
   >>>>>>> "not useful" for addressing Russell's Paradox.   
   >>>>>>   
   >>>>>> ZF or ZFC is to some extent useful for addressing Russell's paradox.   
   >>>>>> It is an example of a set theory where Russell's paradox is avoided.   
   >>>>>> If your "Proof Theretic Semantics" cannot handle the existence of   
   >>>>>> a counter example for every Turing decider then it is not usefule   
   >>>>>> for those who work on practical problems of program correctness.   
   >>>>>   
   >>>>> Proof theoretic semantics addresses Gödel Incompleteness   
   >>>>> for PA in a way similar to the way that ZFC addresses   
   >>>>> Russell's Paradox in set theory.   
   >>>>   
   >>>> Not really the same way. Your "Proof theoretic semantics" redefines   
   >>>> truth and replaces the logic. ZFC is another theory using ordinary   
   >>>> logic. The problem with the naive set theory is that it is not   
   >>>> sound for any semantics.   
   >>>   
   >>> ZFC redefines set theory such that Russell's Paradox cannot arise.   
   >>   
   >> No, it does not. It is just another exammle of the generic concept   
   >> of set theory. Essentially the same as ZF but has one additional   
   >> postulate.   
   >   
   > ZFC redefines set theory such that Russell's Paradox cannot arise   
   > and the original set theory is now referred to as naive set theory.   
      
   ZF and ZFC are not redefinitions. ZF is another theory. It can be   
   called a "set theory" because its structure is similar to Cnator's   
   original informal set theory. Cantor did not specify whther a set   
   must be well-founded but ZF specifies that it must. A set theory   
   were all sets are well-founded does not have Russell's paradox.   
      
   >>> Proof theoretic semantics redefines formal systems such that   
   >>> Incompleteness cannot arise. Gödel did not do this himself because   
   >>> Proof theoretic semantics did not exist at the time.   
   >>   
   >> Gödel did not do that because his topic was Peano arithmetic and its   
   >> extensions, and more generally ordinary logic.   
   >>   
   >> Can you can you prove anyting analogous to Gödel's completeness   
   >> theorem for your "Proof theoretic semantics"?   
      
   Note that the question is not answered (or otherwise addressed) below.   
      
   > Gödel’s incompleteness arises only because   
   > “true in PA” was never an internal notion   
   > of PA at all, but a meta‑mathematical notion   
   > of truth about PA defined externally through   
   > models;   
      
   You have proven neither "only" nor "because".   
      
   > Once truth is defined internally—by extending   
   > PA with a truth predicate so that “true in PA”   
   > simply means “derivable from PA’s axioms”—   
   > the supposed gap between truth and provability   
   > disappears   
      
   But the syntactic incompleteness is still there. Both G and ¬G are   
   well-formed formulas of Peano arithmetic but neither is provable.   
   The well-formed formula G ∨ ¬G is provable, and so is G → G.   
   > With that disappearance PA no longer counts as   
   > incomplete, because the statements Gödel identified   
   > as “true but unprovable” were never internal truths   
   > of PA in the first place, only truths assigned from   
   > the outside by the meta‑system.   
      
   It still is syntactically incomplete.   
      
   --   
   Mikko   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)