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