XPost: sci.math, comp.theory, comp.ai.philosophy   
   From: mikko.levanto@iki.fi   
      
   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'.   
   >   
   > True in the standard model of arithmetic using meta-math   
   > has always been misconstrued as true  arithmetic   
      
   No, it hasn't. In the way theories are usually discussed nothing is   
   "ture in arithmetic". Every sentence of a first order theory that   
   can be proven in the theory is true in every model theory. Every   
   sentence of a theory that cannot be proven in the theory is false   
   in some model of the theory.   
      
      
   [continued in next message]   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)