2026/06/04 by Joseph Vidal-Rosset
Computer Science · Mathematics · #math.LO #cs.LO
Tennant claims that his Core logic ℂ is paraconsistent. It means that the sequent of the First Lewis Paradox, i.e. ¬ A, A \vdash B is declared false, and its corresponding antisequent, called `Claim~1', i.e. ¬ A, A \nvdash B true, as in minimal logic M. 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 F 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.