A Proof in Coq that Core Logic is not Paraconsistent

Abstract

Tennant claims that his Core logic $\mathbb{C}$ is paraconsistent. It means that the sequent of the First Lewis Paradox, i.e. $\neg A,A⊢B$ is declared false, and its corresponding antisequent, called `Claim~1', i.e. $\neg A,A⊬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.

arXiv comment25 pages. Coq, Lean 4 and Athena certifications available online at https://vidal-rosset.net/2026-05-01-core-logic-is-not-paraconsistent.html