XPost: comp.theory   
   From: mikko.levanto@iki.fi   
      
   On 07/02/2026 15:08, 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.   
      
   The question is already answered above: "42" is an input not having   
   a well-founded justification tree, or at least none that I know.   
      
   --   
   Mikko   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)