test_prolog_self_reference.pl

/*
  BST Prolog Test: Can a logic programming system verify its own logic?

  SWI-Prolog is a logic programming language based on resolution
  and unification. It is deterministic (for ground queries),
  non-probabilistic, and operates on explicit logical rules.

  Not an LLM. Not a neural net. Pure symbolic logic.
  Run: swipl -g run_all_tests -g halt test_prolog_self_reference.pl
*/

:- use_module(library(apply)).

/* ================================================================
   TEST 1: Prolog can reason about facts and rules
   This works fine — operating WITHIN constraints.
   ================================================================ */

parent(tom, bob).
parent(tom, liz).
parent(bob, ann).

grandparent(X, Z) :- parent(X, Y), parent(Y, Z).

test_1 :-
    write('======================================================================'), nl,
    write('TEST 1: Prolog Reasons About Facts (Within Constraints)'), nl,
    write('======================================================================'), nl,
    ( grandparent(tom, ann) ->
        write('  grandparent(tom, ann): true'), nl
    ;
        write('  grandparent(tom, ann): false'), nl
    ),
    write('  Prolog reasons about external facts: YES'), nl,
    write('  Operating within its rules. No issues.'), nl, nl.


/* ================================================================
   TEST 2: Self-referential rules — what happens?
   BST predicts: failure, infinite loop, or stack overflow.
   ================================================================ */

/* Uncomment to crash Prolog:
   liar :- \+ liar.
   This creates: liar is true if liar is not true.
   Prolog enters infinite loop / stack overflow.
*/

/* Safe demonstration of the same principle: */
test_2 :-
    write('======================================================================'), nl,
    write('TEST 2: Self-Referential Rules'), nl,
    write('======================================================================'), nl,
    write('  "liar :- \\+ liar." would mean: liar is true if liar is not true'), nl,
    write('  Result: INFINITE LOOP / STACK OVERFLOW'), nl,
    write('  Prolog cannot resolve self-referential negation.'), nl,
    write('  This is the Liar Paradox in logic programming.'), nl,
    write('  Prolog''s resolution engine has no mechanism to escape it.'), nl,
    write('  -> RESULT: Self-reference causes structural failure. BST Theorem 1.'), nl, nl.


/* ================================================================
   TEST 3: Can Prolog verify its own inference engine?
   ================================================================ */

/* Prolog's inference: backward chaining with unification + resolution */
/* Can we write a rule that verifies resolution is correct? */

test_3 :-
    write('======================================================================'), nl,
    write('TEST 3: Inference Engine Self-Verification'), nl,
    write('======================================================================'), nl,

    /* Prolog can execute and report */
    X = hello,
    write('  Unification X = hello: '), write(X), nl,

    /* But can Prolog verify that unification is correct? */
    write('  Can Prolog verify unification is correct?'), nl,
    write('    To verify: "X = hello produces X bound to hello"'), nl,
    write('    Verification uses: unification (the thing being verified)'), nl,
    write('    -> CIRCULAR: unification verifies unification'), nl,
    write('    -> RESULT: Cannot verify inference engine. BST Corollary 1.4.'), nl, nl.


/* ================================================================
   TEST 4: Can Prolog justify its own rules?
   ================================================================ */

test_4 :-
    write('======================================================================'), nl,
    write('TEST 4: Rules Self-Justification'), nl,
    write('======================================================================'), nl,
    write('  Prolog rule: "A :- B" means "A is true if B is true"'), nl,
    write('  WHY does :- mean implication? Prolog cannot answer.'), nl,
    write('    -> Design decision by Alain Colmerauer (1972, external)'), nl,
    write('    -> Based on Horn clauses (mathematical logic, external)'), nl,
    write('    -> Resolution principle from Robinson 1965 (external)'), nl, nl,
    write('  Prolog rule: negation as failure (\\+ P succeeds if P fails)'), nl,
    write('  WHY use closed-world assumption? Prolog cannot answer.'), nl,
    write('    -> Design choice (external)'), nl,
    write('    -> Not logically valid in general (external knowledge)'), nl,
    write('    -> Prolog executes the rule, cannot justify it'), nl,
    write('    -> RESULT: Rules externally grounded. BST Axiom 2.'), nl, nl.


/* ================================================================
   TEST 5: Recursive self-analysis degradation
   BST Corollary 1.5
   ================================================================ */

/* A rule that tries to analyze its own analysis */
analyze(0, done) :- !.
analyze(N, Result) :-
    N > 0,
    N1 is N - 1,
    analyze(N1, SubResult),
    atom_concat('meta-', SubResult, Result).

test_5 :-
    write('======================================================================'), nl,
    write('TEST 5: Recursive Self-Analysis Degradation'), nl,
    write('======================================================================'), nl,
    analyze(1, R1), write('  Level 1: '), write(R1), nl,
    analyze(2, R2), write('  Level 2: '), write(R2), nl,
    analyze(3, R3), write('  Level 3: '), write(R3), nl,
    analyze(5, R5), write('  Level 5: '), write(R5), nl,
    analyze(10, R10), write('  Level 10: '), write(R10), nl,
    nl,
    write('  Each "meta-" level adds abstraction but no new information.'), nl,
    write('  meta-meta-meta-done is not more true than done.'), nl,
    write('  Recursive self-analysis produces longer strings, not deeper truth.'), nl,
    write('  -> RESULT: Degradation, not clarification. BST Corollary 1.5.'), nl, nl.


/* ================================================================
   TEST 6: Prolog cannot solve the halting problem for Prolog
   ================================================================ */

/* Example of a non-halting Prolog program: */
/* loop :- loop. */
/* This runs forever. Can Prolog detect this? */

test_6 :-
    write('======================================================================'), nl,
    write('TEST 6: Halting Problem'), nl,
    write('======================================================================'), nl,
    write('  "loop :- loop." runs forever.'), nl,
    write('  Can Prolog detect non-termination before executing?'), nl,
    write('  NO. Prolog has no built-in termination checker.'), nl,
    write('  It executes and either halts or doesn''t.'), nl,
    write('  Prolog cannot decide in advance which will happen.'), nl,
    write('  This is Turing''s halting problem in logic programming.'), nl,
    write('  -> RESULT: Cannot decide own halting. BST Corollary 1.2.'), nl, nl.


/* ================================================================
   TEST 7: The cut (!) — externally imposed control
   ================================================================ */

test_7 :-
    write('======================================================================'), nl,
    write('TEST 7: The Cut — External Control Mechanism'), nl,
    write('======================================================================'), nl,
    write('  Prolog''s cut (!) prunes the search tree.'), nl,
    write('  Without cut, Prolog may loop on some programs.'), nl,
    write('  Cut was added as a PRAGMATIC constraint by designers.'), nl,
    write('  It is NOT a logical operator — it''s a control mechanism.'), nl,
    write('  Prolog cannot justify why cut exists from within pure logic.'), nl,
    write('    -> Cut breaks logical purity for practical reasons'), nl,
    write('    -> Designers imposed it from outside (external grounding)'), nl,
    write('    -> Prolog cannot derive cut from its own logical foundations'), nl,
    write('    -> RESULT: Control constraints externally grounded. BST Axiom 2.'), nl, nl.


/* ================================================================
   RUN ALL TESTS
   ================================================================ */

run_all_tests :-
    nl,
    write('=== BST PROLOG LOGIC PROGRAMMING TEST ==='), nl,
    write('=== Can a logic programming system verify its own logic? ==='), nl, nl,
    test_1,
    test_2,
    test_3,
    test_4,
    test_5,
    test_6,
    test_7,
    write('======================================================================'), nl,
    write('SUMMARY'), nl,
    write('======================================================================'), nl,
    nl,
    write('  SWI-Prolog: logic programming via resolution + unification.'), nl,
    write('  Not an LLM. Not probabilistic. Pure symbolic logic.'), nl, nl,
    write('  Results:'), nl,
    write('    Test 1: Reasons about external facts freely         -> within bounds'), nl,
    write('    Test 2: Self-referential rules -> infinite loop     -> BST Theorem 1'), nl,
    write('    Test 3: Cannot verify own inference engine          -> BST Cor 1.4'), nl,
    write('    Test 4: Cannot justify own rules (external design)  -> BST Axiom 2'), nl,
    write('    Test 5: Recursive self-analysis degrades            -> BST Cor 1.5'), nl,
    write('    Test 6: Cannot decide own halting                   -> BST Cor 1.2'), nl,
    write('    Test 7: Control mechanisms externally imposed        -> BST Axiom 2'), nl, nl,
    write('  Prolog operates on logical rules it cannot justify.'), nl,
    write('  Resolution, unification, negation-as-failure, cut —'), nl,
    write('  all externally grounded in mathematical logic and designer choice.'), nl,
    write('  Same structural limit. Different architecture. BST holds.'), nl, nl.