• Halting Problem and Proof Theoretic Semantics --- VALIDATED

    From olcott@3:633/10 to All on Sunday, February 01, 2026 21:59:46
    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_Problem_and_Proof_Theoretic_Semantics

    --
    Copyright 2026 Olcott<br><br>

    My 28 year goal has been to make <br>
    "true on the basis of meaning expressed in language"<br>
    reliably computable for the entire body of knowledge.<br><br>

    This required establishing a new foundation<br>


    --- PyGate Linux v1.5.11
    * Origin: Dragon's Lair, PyGate NNTP<>Fido Gate (3:633/10)