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