From: mikko.levanto@iki.fi   
      
   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.   
      
   --   
   Mikko   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)