XPost: sci.logic, sci.math, comp.theory   
   From: mikko.levanto@iki.fi   
      
   On 21/01/2026 17:22, olcott wrote:   
   > On 1/21/2026 3:03 AM, Mikko wrote:   
   >> On 20/01/2026 20:35, olcott wrote:   
   >>> On 1/20/2026 3:58 AM, Mikko wrote:   
   >>>> On 19/01/2026 17:03, olcott wrote:   
   >>>>> On 1/19/2026 2:19 AM, Mikko wrote:   
   >>>>>> 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.   
   >>>>>   
   >>>>> ZF is a redefinition in the only sense that matters:   
   >>>>> it changes the foundational rules so that Russell’s   
   >>>>> paradox cannot arise.   
   >>>>   
   >>>> The only sense that matters is: to give a new meaning to an exsisting   
   >>>> term. That is OK when the new meaning is only used in a context where   
   >>>> the old one does not make sense.   
   >>>>   
   >>>> What you are trying is to give a new meaning to "true" but preted that   
   >>>> it still means 'true'.   
   >>>   
      
   [continued in next message]   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)