XPost: comp.theory, sci.math   
   From: polcott333@gmail.com   
      
   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.   
      
   Is is the same as a truth predicate rejecting   
   True("What time is it?") as not truth-apt.   
      
   --   
   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)