XPost: comp.theory, comp.lang.prolog   
   From: news.x.richarddamon@xoxy.net   
      
   On 1/14/26 7:51 PM, olcott wrote:   
   > On 1/14/2026 6:26 PM, Tristan Wibberley wrote:   
   >> On 15/01/2026 00:14, olcott wrote:   
   >>> The halting problem proof fails ...   
   >>   
   >> Do you mean "The halting problem proof supposition fails ..." ?   
   >>   
   >   
   > The proof does not prove that halting is undecidable.   
   >   
   > By proof‑theoretic semantics I mean the approach in which the   
   > meaning of a statement is determined by its rules of proof   
   > rather than by truth conditions in an external model.   
   > Operational semantics fits this pattern: programs have meaning   
   > through their execution rules, not through abstract denotations.   
   >   
      
   But "Proof-Theoretic Semantics" aren't applicable to the system.   
      
   I guess in you system you can't make a computation that verifies that a   
   proof is correct.   
      
   Your problem is you are not ALLOWED to change the semantics of the   
   system the proof was done in.   
      
   At best, you can say it doesn't apply in other systems, but those system   
   end up being deficent in some needed criteria.   
      
   Being able to handle the properties of the Natural Numbers is one of them.   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)