A Proof in Coq that Core Logic is not Paraconsistent
Joseph Vidal-Rosset
math.LO
Jun 4, 2026 · v3
cs.LO
TL;DR
A Lean 4 twin of the Coq development proves the same twelve statements, checked with Lean Comparator against Lean's kernel and nanoda.
Abstract
Tennant claims that his Core logic $\mathbb{C}$ is paraconsistent. It means that the sequent of the First Lewis Paradox, i.e. $\lnot A, A \vdash B$ is declared false, and its corresponding antisequent, called `Claim 1', i.e. $\lnot A, A \nvdash B$ true, as in minimal logic $\mathbf{M}$. This paper proves that Claim 1 entails a contradiction in $\mathbb{C}$, so that, to preserve consistency, the Core logician must reject the claim that his system is paraconsistent. The proof is purely logical, in four steps within a five-rule fragment $\mathcal{F}$ of $\mathbb{C}$ and its refutation system in the sense of Lukasiewicz and Goranko; the Appendix certifies every step in Coq – with no axiom assumed and every commitment displayed as a named hypothesis – and the same certification is replayed independently in Lean 4.
Problem
Tennant claims his Core logic is paraconsistent, meaning the First Lewis Paradox sequent ¬A, A ⊢ B is not derivable (Claim 1). He also claims Core logic only overlaps minimal logic rather than containing it (Claim 2).
Approach
The argument works in a five-rule fragment of Core logic and its Łukasiewicz–Goranko refutation system. It derives the rules DNS.1 and DNS.2 and proves the invertibility of DNS.1 by structural induction. From that it obtains a refutation rule which, combined with Claim 1, yields a contradiction. The argument is certified in Coq with no axioms and replayed independently in Lean 4, with the proof terms checked by two kernels via Lean Comparator.
Results
Claim 1 entails a contradiction in Core logic, so its paraconsistency claim cannot be sustained. Claim 2 collapses in the same way. The Coq file closes all twelve statements without axioms, and the Lean version depends only on propext.
