Forums before death by AOL, social media and spammers... "We can't have nice things"
|    sci.logic    |    Logic -- math, philosophy & computationa    |    262,912 messages    |
[   << oldest   |   < older   |   list   |   newer >   |   newest >>   ]
|    Message 262,776 of 262,912    |
|    olcott to Richard Damon    |
|    Re: Proof theoretic semantics based halt    |
|    01 Feb 26 11:35:46    |
   
   XPost: comp.theory, sci.math, comp.lang.prolog   
   XPost: sci.lang, comp.software-eng   
   From: polcott333@gmail.com   
      
   On 2/1/2026 6:11 AM, Richard Damon wrote:   
   > On 1/31/26 12:49 PM, olcott wrote:   
   >> Source code of fully operational system   
   >> https://github.com/plolcott/x86utm/blob/master/Halt7.c   
   >>   
   >> int DD()   
   >> {   
   >> int Halt_Status = HHH(DD);   
   >> if (Halt_Status)   
   >> HERE: goto HERE;   
   >> return Halt_Status;   
   >> }   
   >>   
   >> HHH simulates DD step-by-step according to   
   >> the semantics of the C programming language.   
   >   
   > IT CAN'T, as you have been told, as your above program, without the C   
   > CODE for HHH, has undefined behavior by the semantics of the C   
   > programming language.   
   >   
   >>   
   >> HHH correctly determines that DD does not have a well-founded   
   >> justification tree within Proof theoretic semantics.   
   >   
   > But only because your DD is not a well-formed program because you fail   
   > to include the code for all the program.   
   >   
      
   What the f-ck do you think this is? Sheep Dip ?   
   https://github.com/plolcott/x86utm/blob/master/Halt7.c   
      
   > And the reason its behavior isn't "well-founded" is because you failed   
   > to include the actual code for HHH. If you do, and that code happens to   
   > abort its simulation and returns non-halting, then it is well founded   
   > that DD will halt.   
   >   
   >>   
   >> When HHH is construed as a proof theoretic halting prover   
   >> HHH detects the pathological-self-reference of its input and   
   >> rejects DD as non-well-founded on this basis.   
   >   
   > Because your input is just garbage, because you never understood what   
   > you were talking abouyt,   
   >   
   > The problem is you think lying is valid logic.   
   >   
   >>   
   >> % This sentence is not true.   
   >> ?- LP = not(true(LP)).   
   >> LP = not(true(LP)).   
   >> ?- unify_with_occurs_check(LP, not(true(LP))).   
   >> false.   
   >>   
   >> The Liar Paradox is formally rejected by Prolog   
   >> occurs_check for this same reason.   
   >>   
   >> occurs_check correctly determines that LP does not   
   >> have a well-founded justification tree within Proof   
   >> theoretic semantics.   
   >>   
   >   
   > Which is just irrelevent here, as DD doesn't "call" itself.   
   >   
   > Sorry, you are just proving you are just a pathological liar.   
      
      
   --   
   Copyright 2026 Olcott
|
[   << oldest   |   < older   |   list   |   newer >   |   newest >>   ]
(c) 1994, bbs@darkrealms.ca