{"id":"arxiv/2606.05953","url":"https://arxiv.org/abs/2606.05953","tags":["math.LO","cs.LO"],"score":0,"title":"A Proof in Coq that Core Logic is not Paraconsistent","domain":"math.LO","source":"arxiv","authors":["Joseph Vidal-Rosset"],"reviews":0,"subject":"math.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-06-04","reactions":{}}