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}\). Therefore, to preserve consistency, the Core logician must reject \eqref{claim1}, that is to say the claim that his system is paraconsistent.

The proof below is purely logical: four steps in \(\mathcal{F}\), readable without any proof assistant. Every step is certified in Coq and in Lean 4; the last section explains, once the four steps have been read, exactly what the proof files establish and how.

Proof in four steps, in \(\mathcal{F}\) and in its refutation system in the sense of Łukasiewicz and Goranko.

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). These four shared rules constitute \(\mathcal{F}\) under its minimal reading \(\mathcal{F}_{\mathbf{M}}\); adding \(R\to_{\mathbb{C}}\) yields its Core reading \(\mathcal{F}_{\mathbb{C}}\). Every rule of \(\mathcal{F}_{\mathbf{M}}\) is a rule of \(\mathbb{C}\).

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

What do the proof files certify, exactly? Every step of the proof just read. Step 1: DNS.1 and DNS.2 are derivable — DNS.1 uniformly in the two readings of \(\mathcal{F}\), since its derivation uses only the four shared rules, and DNS.2 in \(\mathcal{F}_{\mathbb{C}}\) through \(R\to_{\mathbb{C}}\). Step 2: DNS.1 is invertible in \(\mathcal{F}_{\mathbf{M}}\), by one structural induction on derivations, without Cut. Step 3: the rule \(\overline{DNS.1}\) is a metatheorem of \(\mathcal{F}_{\mathbf{M}}\), proved as the contrapositive of that invertibility — Goranko’s converse-correctness licence [8], mechanised — and the refutation system whose only rejection axiom is \eqref{claim1} and whose only refutation rule is \(\overline{DNS.1}\) is Ł-correct for \(\mathcal{F}_{\mathbf{M}}\): everything it rejects is underivable there. Step 4: the contradiction, certified in two forms — as the Ł-incorrectness of the same refutation system for \(\mathcal{F}_{\mathbb{C}}\), which rejects a sequent that \(\mathcal{F}_{\mathbb{C}}\) derives, and as a conditional theorem (claim1_false) whose two hypotheses, \eqref{claim1} itself and the commitment that the kernel’s refutation rule governs \(\mathbb{C}\)’s rejection assertion, are displayed rather than hidden. The proof above is therefore not illustrated by the machine after the fact: it is covered by it, step by step; and whoever wishes to resist the conclusion must reject one of the two displayed hypotheses — at the price, for the second, of giving up the refutation discipline of the very kernel that grounds the overlap of \(\mathbb{C}\) with \(\mathbf{M}\).

The Theorem receives its certified proofs in

• Coq,
• Lean Comparator Live (Experimental),
• Athena (which certifies the earlier presentation of the argument; its update to the present version is in progress);

and the Corollary follows by the same reasoning, mutatis mutandis.

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 establishes the invertibility of DNS.1 and the rule \(\overline{DNS.1}\) as metatheorems of \(\mathcal{F}_{\mathbf{M}}\) by structural induction on derivations, formalizes the refutation system itself — \eqref{claim1} as its only rejection axiom, \(\overline{DNS.1}\) as its only refutation rule — and certifies its two verdicts: Ł-correctness for \(\mathcal{F}_{\mathbf{M}}\) and Ł-incorrectness for \(\mathcal{F}_{\mathbb{C}}\). Its Print Assumptions command makes its whole axiomatic basis auditable — it reports that every theorem is closed under the global context: nothing is assumed, the two principles the argument grants to Tennant being explicit hypotheses of the final theorem.

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 very same argument: the two principles granted to Tennant are, exactly as in the Coq script, named hypotheses of its final theorem. The certified statement is therefore a pure conditional — Tennant’s Claim 1, together with the commitment that the kernel’s refutation rule \(\overline{DNS.1}\) governs \(\mathbb{C}\)’s rejection assertion (hypothesis anti_DNS1_rule_for_ℂ, named conservativity_at_DNS1 in the Version 4 files), 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 two hundred lines stating the language, the rules of \(\mathcal{F}\) under its two readings, the refutation system Refutable, and the twelve certified statements — the derivability of DNS.1 and DNS.2, the invertibility of DNS.1 in \(\mathcal{F}_{\mathbf{M}}\) together with the underivability of both sides of its decisive instance, \(\overline{DNS.1}\), the Ł-correctness and Ł-incorrectness verdicts, the two conditional collision theorems, and the two theorems settling the status of the second hypothesis (claim1_holds_in_ℱ_ℂ and anti_DNS1_Ł_incorrect_for_ℱ_ℂ, the latter named ℱ_ℂ_not_conservative_at_DNS1 in Versions 4 and 5) — is the entire trusted base of that check (SHA256: 6147a4234a2420a420d2c67eb145ace7b3d9ec14fc1e2dc368c35010e54804cc). 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, for the final theorem:

'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.