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