XPost: comp.theory, sci.math, comp.lang.prolog   
   XPost: comp.software-eng   
   From: polcott333@gmail.com   
      
   On 1/14/2026 3:04 AM, Mikko wrote:   
   > On 13/01/2026 16:17, olcott wrote:   
   >> On 1/13/2026 2:46 AM, Mikko wrote:   
   >>> On 12/01/2026 16:43, olcott wrote:   
   >>>> On 1/12/2026 4:51 AM, Mikko wrote:   
   >>>>> On 11/01/2026 16:23, olcott wrote:   
   >>>>>> On 1/11/2026 4:22 AM, Mikko wrote:   
   >>>>>>> On 10/01/2026 17:47, olcott wrote:   
   >>>>>>>> On 1/10/2026 2:23 AM, Mikko wrote:   
   >>>>>>>>> On 09/01/2026 17:52, olcott wrote:   
   >>>>>>>>>> On 1/9/2026 3:59 AM, Mikko wrote:   
   >>>>>>>>>>> On 08/01/2026 16:22, olcott wrote:   
   >>>>>>>>>>>> On 1/8/2026 4:22 AM, Mikko wrote:   
   >>>>>>>>>>>>> On 07/01/2026 13:54, olcott wrote:   
   >>>>>>>>>>>>>> On 1/7/2026 5:49 AM, Mikko wrote:   
   >>>>>>>>>>>>>>> On 07/01/2026 06:44, olcott wrote:   
   >>>>>>>>>>>>>>>> All deciders essentially: Transform finite string   
   >>>>>>>>>>>>>>>> inputs by finite string transformation rules into   
   >>>>>>>>>>>>>>>> {Accept, Reject} values.   
   >>>>>>>>>>>>>>>>   
   >>>>>>>>>>>>>>>> The counter-example input to requires more than   
   >>>>>>>>>>>>>>>> can be derived from finite string transformation   
   >>>>>>>>>>>>>>>> rules applied to this specific input thus the   
   >>>>>>>>>>>>>>>> Halting Problem requires too much.   
   >>>>>>>>>>>>>>   
   >>>>>>>>>>>>>>> In a sense the halting problem asks too much: the problem   
   >>>>>>>>>>>>>>> is proven to   
   >>>>>>>>>>>>>>> be unsolvable. In another sense it asks too little:   
   >>>>>>>>>>>>>>> usually we want to   
   >>>>>>>>>>>>>>> know whether a method halts on every input, not just one.   
   >>>>>>>>>>>>>>>   
   >>>>>>>>>>>>>>> Although the halting problem is unsolvable, there are   
   >>>>>>>>>>>>>>> partial solutions   
   >>>>>>>>>>>>>>> to the halting problem. In particular, every counter-   
   >>>>>>>>>>>>>>> example to the   
   >>>>>>>>>>>>>>> full solution is correctly solved by some partial deciders.   
   >>>>>>>>>>>>>>   
   >>>>>>>>>>>>>> *if undecidability is correct then truth itself is broken*   
   >>>>>>>>>>>>>   
   >>>>>>>>>>>>> Depends on whether the word "truth" is interpeted in the   
   >>>>>>>>>>>>> standard   
   >>>>>>>>>>>>> sense or in Olcott's sense.   
   >>>>>>>>>>>>   
   >>>>>>>>>>>> Undecidability is misconception. Self-contradictory   
   >>>>>>>>>>>> expressions are correctly rejected as semantically   
   >>>>>>>>>>>> incoherent thus form no undecidability or incompleteness.   
   >>>>>>>>>>>   
   >>>>>>>>>>> The misconception is yours. No expression in the language of   
   >>>>>>>>>>> the first   
   >>>>>>>>>>> order group theory is self-contradictory. But the first order   
   >>>>>>>>>>> goupr   
   >>>>>>>>>>> theory is incomplete: it is impossible to prove that AB = BA   
   >>>>>>>>>>> is true   
   >>>>>>>>>>> for every A and every B but it is also impossible to prove   
   >>>>>>>>>>> that AB = BA   
   >>>>>>>>>>> is false for some A and some B.   
   >>>>>>>>>>>   
   >>>>>>>>>>   
   >>>>>>>>>> All deciders essentially: Transform finite string   
   >>>>>>>>>> inputs by finite string transformation rules into   
   >>>>>>>>>> {Accept, Reject} values.   
   >>>>>>>>>>   
   >>>>>>>>>> When a required result cannot be derived by applying   
   >>>>>>>>>> finite string transformation rules to actual finite   
   >>>>>>>>>> string inputs, then the required result exceeds the   
   >>>>>>>>>> scope of computation and must be rejected as an   
   >>>>>>>>>> incorrect requirement.   
   >>>>>>>>>   
   >>>>>>>>> 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.   
   >>>>>>>>   
   >>>>>>>>> Of course, it one can prove that the required result is not   
   >>>>>>>>> computable   
   >>>>>>>>> then that helps to avoid wasting effort to try the impossible. The   
   >>>>>>>>> situation is worse if it is not known that the required result   
   >>>>>>>>> is not   
   >>>>>>>>> computable.   
   >>>>>>>>>   
   >>>>>>>>> That something is not computable does not mean that there is   
   >>>>>>>>> anyting   
   >>>>>>>>> "incorrect" in the requirement.   
   >>>>>>>>   
   >>>>>>>> Yes it certainly does. Requiring the impossible is always an error.   
   >>>>>>>   
   >>>>>>> It is a perfectly valid question to ask whther a particular   
   >>>>>>> reuqirement   
   >>>>>>> is satisfiable.   
   >>>>>>   
   >>>>>> Any yes/no question lacking a correct yes/no answer   
   >>>>>> is an incorrect question that must be rejected on   
   >>>>>> that basis.   
   >>>>>   
   >>>>> Irrelevant. The question whether a particular requirement is   
   >>>>> satisfiable   
   >>>>> does have an answer that is either "yes" or "no". In some ases it is   
   >>>>> not known whether it is "yes" or "no" and there may be no known way to   
   >>>>> find out be even then either "yes" or "no" is the correct answer.   
   >>>>   
   >>>> Now that I finally have the standard terminology:   
   >>>> Proof-theoretic semantics has always been the correct   
   >>>> formal system to handle decision problems.   
   >>>>   
   >>>> When it is asked a yes/no question lacking a correct   
   >>>> yes/no answer it correctly determines non-well-founded.   
   >>>> I have been correct all along and merely lacked the   
   >>>> standard terminology.   
   >>>   
   >>> Irrelevant, as already noted above.   
   >>   
   >> It is not irrelevant at all. Most all of undecidability   
   >> cease to exist in this system:   
   >   
   > It does not help if the system is not sound. Or if the particuar   
   > undecidability that one happens to care about does not cease to   
   > exist.   
   >   
      
   Soundness is exactly why proof‑theoretic semantics matters here.   
   When meaning is grounded in inferential structure and truth is anchored   
   in an axiomatic base, only well‑founded expressions are admissible. The   
   classical undecidability constructions (Halting, Gödel, Tarski, Curry)   
   all rely on expressions whose semantic dependency graphs contain cycles.   
   Those expressions are not well‑formed truthbearers in a sound, grounded   
   system, so the corresponding undecidability results do not arise.   
      
   --   
   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)