A Triple Certified Proof that Core Logic is not Paraconsistent

The theory according to which \(\mathbb{C}\) is paraconsistent is false, because \eqref{claim1} entails a contradiction in \(\mathbb{C}\).

Proof in four steps in \(\mathcal{F}\)

Table 1 reproduces a fragment \(\mathcal{F}\) of the rules of \(\mathbb{C}\) [1, pp. 159–163]. The label \(R\to_{\mathbb{C}}\) is mine, not Tennant’s; I use it because it is the only Core-specific rule in \(\mathcal{F}\), the other four being exactly the same as in minimal logic (for short, M).

Two remarks:

1. In this syntax, \[\Delta \vdash B\] presupposes that \(\Delta\) is consistent, otherwise \[\Delta \vdash\] must be written.

2. In textbooks, rule \(R\to\) is usually written as

The unusual form of rule \(R\to\) in Table 1 means that, with consistent contexts, the discharge of A is optional.

Tennant claims that this second antisequent

is also true in Core logic, by contrast with M, which explains that in the Figure of logical system inclusions [1, p. 35] Tennant draws an overlap of \(\mathbb{C}\) on M. But, this is a mistake, because such a claim entails the same inconsistency, hence this corollary of the previous theorem:

\eqref{claim2} is false, therefore it cannot establish correctly that \(\mathbb{C}\) overlaps minimal logic.

Proof. \eqref{claim2} meets exactly the same contradiction:

Therefore, \eqref{claim2} is false and cannot establish correctly that \(\mathbb{C}\) overlaps minimal logic. \(\blacksquare\)

The Theorem and its Corollary share the same certification in

• Coq,
• Lean 4 with Comparator Live session,
• Athena.

These certifications differ in their logical foundations, and that difference is precisely their joint interest. The Coq script is the reference version: built on dependent type theory, it proves the invertibility of DNS.1 by structural induction on derivations in \(\mathcal{F}\), and its Print Assumptions command makes its whole axiomatic basis auditable — it reports exactly the two principles the argument grants to Tennant, with nothing else assumed. The Lean 4 file is a port of that script into another kernel of the same type-theoretic family; written in pure core Lean 4, without any Mathlib dependency, it can be re-checked in the browser at the link above, with nothing to install.

It presents the same argument in an equivalent form, by the deduction theorem: the two principles granted to Tennant, posited as global Axioms in the Coq script, are internalised as named hypotheses of its final theorem. The certified statement is therefore a pure conditional — Tennant’s Claim 1, together with the transfer of antisequent rules from \(\mathbf{M}\) to \(\mathbb{C}\) on their shared fragment, jointly entails absurdity — resting on no non-logical axiom at all, as #print axioms reports.

This conditional form allows a further, independent layer of verification. The Lean proof has been validated with the Lean Comparator, the Lean project’s tool for checking a proof against a trusted challenge: the challenge states the theorem, and the comparator verifies that the candidate solution proves exactly that statement, using no axiom beyond Lean’s three built-ins. The challenge file — some seventy-five lines stating the language, the rules of \(\mathcal{F}\), and the conditional theorem — is the entire trusted base of that check (SHA256: f3b8542d785b97688e56d8d617b4bf69dbfab7ef6678fb35dbe4d9cfa6cbd222). Nothing in the solution file itself needs to be read, or even trusted: whatever that file contains, the comparator guarantees that it proves exactly the statement of the challenge — neither a weaker one, nor a cleverly disguised one — and that it smuggles in no axiom.

Beyond that one-click check, the Lean proof has been validated at the gold standard of the Lean reference manual: built in a sandbox and exported to a serialised proof term, it was replayed through two independently implemented kernels — Lean’s own and nanoda, written in Rust. On the author’s machine the command-line comparator reports:

Solution.lean:453:0: 'claim1_false' depends on axioms: [propext]
Build completed successfully (3 jobs).
Running nanoda kernel on solution
Nanoda kernel accepts the solution
Running Lean default kernel on solution.
Lean default kernel accepts the solution
Your solution is okay!

Both kernels accept the proof term, whose only axiom is propext; the statement they accept is, by construction, exactly that of the trusted challenge. The result therefore depends neither on a single formalism, nor on the author’s good faith, nor on the correctness of any one kernel.

If you wish to reproduce this locally on your own machine, the challenge, the solution and the comparator configuration are provided in my Github repository: install a Lean toolchain with elan, build comparator with the nanoda kernel enabled, and run it on that configuration as described in the reference manual above.

Athena, by contrast, rests on a different paradigm altogether: a denotational proof language over many-sorted first-order logic, driven by automated provers rather than by a type-theoretic kernel. That the same contradiction is certified in two dependent type theories and in a first-order denotational language shows that this proof owes nothing to the idiosyncrasies of a single system: it is the logical result of the conjunction of the small fragment \(\mathcal{F}\) of \(\mathbb{C}\) and \eqref{claim1}, not an artefact of a specific formalism. The three source files are available on GitHub.