How Prolog corroborates the proof that Core Logic is not paraconsistent

The companion document Correspondence of the Fragment F rules already lines up Table 1 against Coq, Lean, Athena and Prolog, clause by clause. Here I only drive the nail: I take the Coq declaration and show, first, that the Prolog engine runs the same five rules, and second — the decisive point — that these five are all the rules there are.

The Coq derivability relation is one Inductive with exactly five constructors:

Inductive derivable :
  fragment_F -> set formula -> option formula -> Prop :=
| Ax          : forall f G A,     In A G -> derivable f G (Some A)
| L_neg       : forall f G A,     In (Neg A) G -> derivable f G (Some A) -> derivable f G None
| R_arrow     : forall f G A B,   derivable f (A :: G) (Some B) -> derivable f G (Some (Impl A B))
| L_arrow     : forall f G A B C, In (Impl A B) G -> derivable f G (Some A) -> derivable f (B :: G) C -> derivable f G C
| R_arrow_core: forall G A B,     derivable core_logic (A :: G) None -> derivable core_logic G (Some (Impl A B)).

The Prolog engine has one axiom clause and four rule clauses — one for each remaining constructor:

ax(Gamma:A) :- A \= (_=>_), A \= bot, iso_member(A, Gamma).       % Ax

rules(lneg,       Gamma:bot,   Rest:A)          :- iso_select(~A, Gamma, Rest).   % L¬
rules(rcond,      Gamma:A=>B,  [A|Gamma]:B)     :- B \= bot.                       % R→
rules(rcond_core, Gamma:A=>_B, [A|Gamma]:bot).                                     % R→C
rules(lcond,      Gamma:C,     conj(Rest:A, [B|Rest]:C)) :- iso_select(A=>B, Gamma, Rest). % L→

Read the two side by side and the map is total and injective both ways: ax ↔ Ax, lneg ↔ L_neg, rcond ↔ R_arrow, rcond_core ↔ R_arrow_core, lcond ↔ L_arrow. The membership form (iso_member, iso_select) is Coq’s In A G to the letter; the empty succedent that Coq writes None is the object constant bot in succedent position; a conditional identity is derived, not initial, which is exactly why the axiom clause guards A \ (=>)=. These are encoding conventions, set out in the companion note, not extra rules.

The decisive move is the closure argument, and it belongs to the kind of object an Inductive is. An inductive definition is closed: its constructors are the only ways to build an inhabitant. So Coq’s five constructors are not “five rules among others we happen to use” — they are, provably, every way a sequent can be derived in \(\mathcal{F}\). Print Assumptions confirms the definition is closed under the global context. The Prolog side has, correspondingly, exactly five heads — ax/1 plus four rules/3 clauses — and no more. There is nowhere for a hidden rule to hide: an objector who suspects the underivability of the Claims is an artifact of some smuggled-in principle can enumerate the clauses and find that the list is closed, finite, and identical to Table 1. The first four rules are parametric in the fragment f (they hold under the minimal reading \(\mathcal{F}_{\mathbf M}\) and the Core reading \(\mathcal{F}_{\mathbb C}\) alike); only rcond_core is restricted to core_logic. That single Core-specific rule is the whole of the extra strength Core grants over the minimal fragment — and, as the theorem shows, the whole of what breaks the symmetry on the fatal sequent.

A skeptic’s natural worry: perhaps the engine fails on \(\lnot A, A \vdash B\) simply because it is too weak to prove anything interesting — in which case the failure would be worthless. This door closes with a single run. Take the formula the anonymous correspondent himself put forward, \[ (p \to (q \to r)) \to (q \to (p \to r)), \] the permutation-of-antecedents theorem — a genuine theorem of minimal (indeed of pure implicational) logic. Consult the file and click: the engine answers PROVABLE and draws its tree — built, and rendered, by the very clauses that compute it.

?- prove.

Two things about this derivation matter. First, it uses only ax, rcond and lcond — that is, only Ax, \(R\to\) and \(L\to\). No \(L\lnot\), and crucially no rcond_core: the theorem lives squarely in the minimal fragment \(\mathcal{F}_{\mathbf M}\), with no appeal to the one Core-specific rule and none whatever to ex falso. (One can check this mechanically: the tree carries no \(L\lnot\) and no \(R\to_{\mathbb C}\) step.) Second, note that the file’s fragment. command already verifies the sequent form \(A\to(B\to C) \vdash B \to (A \to C)\); the correspondent’s formula is just its fully-discharged, theorem-form cousin. His challenge formula was, in essence, already in the test suite.

So the engine is not impotent: it proves the theorems minimal logic ought to prove, by the rules of \(\mathcal{F}\), and it does so using only the sub-fragment that excludes ex falso. When that same engine then fails on \(\lnot A, A \vdash B\), the failure is discriminating. It is not “this system proves nothing”; it is “this system proves the genuine theorems and refuses precisely ex-falso-shaped sequents” — which is exactly the behaviour that makes \(\mathcal{F}\) a fragment of minimal, and not of intuitionistic, logic.

The command main. walks the article. I follow the same order, showing at each step the machine’s own output, so that a reader can run the file and read the paper in parallel.

There is a last worry an objector could raise about the search itself: the default engine (main.) uses permissive axioms that admit weakening on the left at the leaves, for efficiency. Does that permissiveness taint the verdicts? No — for two reasons.

First, the weakening is less un-Core than it looks. Left-weakening — adjoining an unused hypothesis to the context — is not a primitive rule of \(\mathbb C\), but it is Core-admissible in exactly the regime these sequents inhabit: so long as the context is not explicitly inconsistent and no derivation of \(\lnot A, A \vdash \lnot B\) is in play. Its propositional witness is that \(A \vdash B \to A\) is Core-provable — Tennant’s vacuous discharge, the diamond on the discharge stroke, which the strict run derives explicitly as \(B \vdash A \to B\) [1, p. 35]. The one regime where left-weakening would be genuinely illicit in Core is the inconsistent context, where unrestricted weakening would simply be ex falso — and that is exactly the case Core is built to refuse, and exactly the case the weakening-free strict run re-checks below. The permissive axiom is thus a matter of efficiency, not a smuggled-in non-Core principle.

Second, the two modes bracket the result from opposite sides. The permissive engine proves a superset of what strict Core proves (weakening only adds derivations). Therefore, for the negative results, permissive failure is the stronger fact: if even the weakening-admitting engine cannot derive \(\lnot A, A \vdash B\), then strict Core — a fortiori — cannot. The over-approximation makes the antisequents more robust, not less. For the positive results, one wants the opposite guarantee, and core_strict. supplies it: with strictly singleton axioms \([C]:C\), explicit context-splitting on \(L\to\), and Tennant’s diamond on the discharge stroke (2017, p. 21), it re-derives the load-bearing sequents without any weakening at all:

A |- A                                   : DERIVABLE (strict Core OK)
|- A => A                                : DERIVABLE (strict Core OK)
A=>B, A |- B                             : DERIVABLE (strict Core OK)
B |- A=>B         (R-> vacuous)          : DERIVABLE (strict Core OK)
~A, A |-          (L~ on axiom)          : DERIVABLE (strict Core OK)
~A |- A=>B        (DNS.2 left premiss)   : DERIVABLE (strict Core OK)
(A=>B)=>B, ~A |- B      (DNS.2 concl.)   : DERIVABLE (strict Core OK)
(A=>~B)=>~B, ~A |- ~B   (Corollary)      : DERIVABLE (strict Core OK)

~A, A |- B    (Claim 1, must fail)       : NOT DERIVABLE (as expected)
~A, A |- ~B   (Claim 2, must fail)       : NOT DERIVABLE (as expected)

Permissive search = an upper bound on provability, under which the Claims still fail; strict run = a lower bound, under which the positive derivations still succeed. The result holds at both ends. (The one line worth writing out for the reader who wants it airtight: strict-provable \(\subseteq\) permissive-provable, since permissive weakening subsumes the vacuous-discharge case that strict adds; hence permissive failure transfers to strict.)

To close without overclaiming: the one inference the model cannot make on its own is the step from “no derivation of depth \(\le 6\) was found” to “no derivation exists”. That the bound is adequate for these shallow sequents is an argument about the search space, made outside Prolog — and it is exactly the inference the three kernels replace by taking the antisequent as an audited hypothesis. That is the seam between corroboration and certification, and it is the only one. Everything on the Prolog side of it — the rules are \(\mathcal{F}\) and all of \(\mathcal{F}\); the rules prove the real theorems; the two branches of the contradiction are searched for and constructed before one’s eyes — is a finite, runnable, exhibitable fact.

Nothing here needs to be taken on trust: consult core_logic_is_not_paraconsistent.pl at SWI-Tinker (in the browser, nothing to install) and type main., or any single command — fragment., dns_rules., dns1_sem_inv., dns1_inv_cut., dns1_anti., theorem., corollary., core_strict.. All sources — the three frozen certifications and this Prolog model — are in the GitHub repository; the certifications are untouched and their SHA256 hashes unchanged.

— for Jan Wielemaker, again: the model runs where it does because SWI-Prolog runs where it does.