A Proof in Coq that Core Logic is not Paraconsistent
arXiv:2606.05953
The paper formalizes a fragment of Tennant's Core logic in Coq and Lean, proving that Core logic is not paraconsistent and exposing a contradiction in its claimed overlap with minimal logic.
Abstract
Tennant claims that his Core logic is paraconsistent. It means that the sequent of the First Lewis Paradox, i.e. is declared false, and its corresponding antisequent, called `Claim~1', i.e. true, as in minimal logic . This paper proves that Claim~1 entails a contradiction in , 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 of 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.
25 pages. Coq, Lean 4 and Athena certifications available online at https://vidal-rosset.net/2026-05-01-core-logic-is-not-paraconsistent.html