XPost: comp.lang.c++, comp.lang.prolog, comp.ai.philosophy
From: polcott333@gmail.com

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.

HHH correctly determines that DD does not have
a well-founded justification tree within Proof
theoretic semantics.

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.

% 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




All five LLM systems agree with the above
this one is the most succinct agreement:

*Halting Problem and Proof Theoretic Semantics*
https://philpapers.org/archive/OLCHPA.pdf

https://philpapers.org/rec/OLCHPA

https://www.researchgate.net/publication/400341134_Halting_Probl
m_and_Proof_Theoretic_Semantics

--
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)