XPost: comp.theory   
   From: polcott333@gmail.com   
      
   On 2/7/2026 8:44 AM, Richard Damon wrote:   
   > On 2/7/26 8:08 AM, olcott wrote:   
   >> On 2/7/2026 4:15 AM, Mikko wrote:   
   >>> On 06/02/2026 17:32, olcott wrote:   
   >>>> On 2/6/2026 3:15 AM, Mikko wrote:   
   >>>>> On 05/02/2026 13:28, olcott wrote:   
   >>>>>   
   >>>>>> On 2/5/2026 4:45 AM, Mikko wrote:   
   >>>>>>> On 04/02/2026 18:47, olcott wrote:   
   >>>>>>>   
   >>>>>>>> A halt prover attempts to prove halting   
   >>>>>>>   
   >>>>>>> To prove that a computation halts is simple. Just show the execution   
   >>>>>>> trace from the start to the halting. The hard problem is to prove   
   >>>>>>> that an execution does not halt.   
   >>>>>>>   
   >>>>>>>> and when it detects that the proof of its input does not form   
   >>>>>>>>   
   >>>>>>>> *a well-founded justification tree within Proof*   
   >>>>>>>> *theoretic semantics*   
   >>>>>>>>   
   >>>>>>>> Then it is correct to reject this input as bad data.   
   >>>>>>>   
   >>>>>>> No, that does not follow. That only means that it is correct to   
   >>>>>>> reject   
   >>>>>>> the proof. The conclusion of the proof may still be correct.   
   >>>>>> The way that proofs work in proof theoretic   
   >>>>>> semantics is that they reject inputs not having   
   >>>>>> well-founded justification trees as bad data.   
   >>>>>   
   >>>>> An example of a valid input is "42". That input has no justification,   
   >>>>> well-founded or otherwise. But there is no proof that would reject   
   >>>>> "42" as bad data.   
   >>>>   
   >>>> It is an element of the set of natural numbers.   
   >>>   
   >>> True, but non necessarily relevant to tthe proof. But the current   
   >>> question is whether the proof rejects the input "42" as bad data.   
   >>>   
   >>   
   >> Is the integer 42 a machine description that halts?   
   >> Reject.   
   >>   
   >   
   > But 42 might well be a machine description that halts, it depend on how   
   > you have defined your encoding of a machine.   
      
   Can't be the shortest one is a single quintuple.   
      
   --   
   Copyright 2026 Olcott

   
      
   My 28 year goal has been to make 
   
   "true on the basis of meaning expressed in language"
   
   reliably computable for the entire body of knowledge.

   
      
   This required establishing a new foundation
   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)