Delphi.science

A Proof in Coq that Core Logic is not Paraconsistent

Joseph Vidal-Rosset

arXivarxiv/2606.05953Jun 4, 2026math.LOscore 0

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…

SourceJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/arxiv/2606.05953
curl -X POST /api/v1/records/arxiv/2606.05953/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2606.05953/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'