XPost: sci.math, comp.theory, comp.ai.philosophy   
   From: polcott333@gmail.com   
      
   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.   
      
   >> 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"?   
   >   
      
      
   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;   
      
   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   
      
   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.   
      
   --   
   Copyright 2026 Olcott

   
      
   My 28 year goal has been to make 
   
   "true on the basis of meaning expressed in language"
   
   reliably computable.

   
      
   This required establishing a new foundation
   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)