A Triple Certified Proof that Core Logic is not Paraconsistent
Table of Contents
This note provides a proof that Tennant’s two claims — that his own logical system is paraconsistent, and that it overlaps minimal logic — are both false. This proof is triple certified: by Coq, by Lean 4 and by Athena.
Tennant has invented a logical system that he calls “Core logic” (for short, \(\mathbb{C}\)) and that he claims paraconsistent [1, p. 156], that is to say, in agreement with the negative definition of paraconsistency, a system in which the sequent
\begin{equation} \label{eq:1} \lnot A, A \vdash B \end{equation}is false, i.e. its corresponding antisequent, in other words, its negation represented as follows
\begin{equation} \lnot A, A \nvdash B \tag{Claim 1}\label{claim1} \end{equation}is true, like in minimal logic (for short, M). Tennant indeed asserts this semantic antisequent himself [1, p. 186]:
\begin{equation} \label{eq:2} \lnot A, A \nvDash B \end{equation}Assuming that \(\mathbb{C}\) is sound \eqref{claim1} is thus granted on Tennant’s own terms. But the following unexpected theorem makes his paraconsistency theory indefensible:
1. Theorem
The theory according to which \(\mathbb{C}\) is paraconsistent is false, because \eqref{claim1} entails a contradiction in \(\mathbb{C}\).
Proof in four steps in \(\mathcal{F}\)
| \begin{prooftree} \AxiomC{} \RightLabel{\scriptsize{\textit{Ax.}}} \UnaryInfC{$A \vdash A$} \end{prooftree} | ||
| \begin{prooftree} \AxiomC{$\Delta \vdash A$} \RightLabel{\scriptsize{$L\lnot$}} \UnaryInfC{$\lnot A, \Delta \vdash$} \end{prooftree} | \begin{prooftree} \AxiomC{$\Delta \vdash B$} \RightLabel{\scriptsize{$R\to$}} \UnaryInfC{\(\Delta \backslash \{A\} \vdash A \to B\)} \end{prooftree} | |
| \begin{prooftree} \AxiomC{$\Delta \vdash A$} \AxiomC{$B, \Gamma \vdash C$} \RightLabel{\scriptsize{$L\to$}} \BinaryInfC{$A \to B, \Delta, \Gamma \vdash C$} \end{prooftree} | \begin{prooftree} \AxiomC{$A, \Delta \vdash$} \RightLabel{\scriptsize{\(R\to_{\mathbb{C}}\)}} \UnaryInfC{$\Delta \vdash A \to B$} \end{prooftree} |
Table 1 reproduces a fragment \(\mathcal{F}\) of the rules of \(\mathbb{C}\) [1, pp. 159–163]. The label \(R\to_{\mathbb{C}}\) is mine, not Tennant’s; I use it because it is the only Core-specific rule in \(\mathcal{F}\), the other four being exactly the same as in minimal logic (for short, M).
Two remarks:
1. In this syntax, \[\Delta \vdash B\] presupposes that \(\Delta\) is consistent, otherwise \[\Delta \vdash\] must be written.
2. In textbooks, rule \(R\to\) is usually written as
\begin{prooftree} \AxiomC{$A, \Delta \vdash B$} \RightLabel{\scriptsize{$R\to$}} \UnaryInfC{$\Delta \vdash A \to B$} \end{prooftree}The unusual form of rule \(R\to\) in Table 1 means that, with consistent contexts, the discharge of A is optional.
1.1. DNS.1 and DNS.2 are derivable
`DNS’ being an acronym for `Double Negation à la Slaney’ [2], I call `DNS.1’ and `DNS.2’ the rules listed in Table 2 below, together with their respective derivations in \(\mathcal{F}\), which prove that they are derivable in \(\mathbb{C}\). (By definition, a rule is derivable in a given system of rules if its conclusion is derivable from its premisses within the system [3, p. 47].)
| \begin{prooftree}\AxiomC{$A, \Delta \vdash B$}\RightLabel{\scriptsize{DNS.1}}\UnaryInfC{$(A \to B) \to B, \Delta \vdash B$}\end{prooftree} | \begin{prooftree}\AxiomC{$A, \Delta \vdash$}\RightLabel{\scriptsize{DNS.2}}\UnaryInfC{$(A \to B) \to B, \Delta \vdash B$}\end{prooftree} | |
| \begin{prooftree}\AxiomC{$A, \Delta \vdash B$}\RightLabel{\scriptsize{$R\to$}}\UnaryInfC{$\Delta \vdash A \to B$}\AxiomC{} \RightLabel{\scriptsize{$Ax$}}\UnaryInfC{$B \vdash B$}\RightLabel{\scriptsize{$L\to$}}\BinaryInfC{$(A \to B) \to B, \Delta \vdash B$}\end{prooftree} | \begin{prooftree}\AxiomC{$A, \Delta \vdash$}\RightLabel{\scriptsize{\(R\to_{\mathbb{C}}\)}}\UnaryInfC{$\Delta \vdash A \to B$} \AxiomC{}\RightLabel{\scriptsize{$Ax$}}\UnaryInfC{$B \vdash B$}\RightLabel{\scriptsize{$L\to$}}\BinaryInfC{$(A \to B) \to B, \Delta \vdash B$}\end{prooftree} |
1.2. DNS.1 is invertible
A rule is invertible when, from the derivability of a sequent of the form of its conclusion, the derivability of all its premisses follows [4, p. 93]. By inspection of the derivation of DNS.1 in Table 2 above, it is provable in \(\mathcal{F}\) that DNS.1 is invertible.
Indeed, from root to top, this derivation starts from an application of rule \(L\to\), whose invertibility of the deduction on the right is trivial. On the left of this derivation, there is an application of rule \(R\to\). Consequently, DNS.1’s invertibility depends on \(R\to\)’s, which is provable in turn. Note that in his discussion of the converse of the Deduction theorem, Tennant himself acknowledged the invertibility of \(R\to\) [1, p. 46] and, because the context of \(R\to\) is assumed as consistent, the application of Cut i.e.
\begin{prooftree} \AxiomC{$\Delta \vdash A \to B$} \AxiomC{} \RightLabel{\scriptsize{$Ax$}} \UnaryInfC{$A \vdash A$} \AxiomC{} \RightLabel{\scriptsize{$Ax$}} \UnaryInfC{$B \vdash B$} \BinaryInfC{$A \to B, A \vdash B$} \RightLabel{\scriptsize{$Cut$}} \BinaryInfC{$\Delta, A \vdash B$} \end{prooftree}is \(\mathbb{C}\)-admissible in this case [1, p. 154] and therefore impossible to deny. Note also that, provably valid in M, DNS.1 containing no negation, its invertibility cannot be invalid in \(\mathbb{C}\); but, for the most skeptical reader, in mechanised proofs whose links are given at the end of this note, an invertibility proof for DNS.1 is done by structural induction on derivation trees in \(\mathcal{F}\). The \(\mathbb{C}\)-admissibility of Cut makes this proof of invertibility easy, by contrast with the structural induction, which is longer and harder but appeals to no Cut at all. Either way, DNS.1 is both derivable and invertible in \(\mathbb{C}\).
1.3. Deduction of \(\overline{DNS.1}\)
The invertibility of DNS.1 means that whenever the conclusion is derivable, the premiss is derivable too. By contraposition, whenever the premiss is not derivable, the conclusion is not derivable either. This is precisely the rule \(\overline{DNS.1}\):
\begin{prooftree} \AxiomC{$A, \Delta \nvdash B$} \RightLabel{\scriptsize{$\overline{DNS.1}$}} \UnaryInfC{$(A \to B) \to B, \Delta \nvdash B$} \end{prooftree}1.4. Deduction of the contradiction
This point is the conclusion of the proof: as premiss of \(\overline{DNS.1}\), \eqref{claim1} entails an antisequent which is in contradiction with a consequence of DNS.2:
\begin{prooftree} \AxiomC{} \RightLabel{\scriptsize{(Claim 1)}} \UnaryInfC{$\lnot A, A \nvdash B$} \RightLabel{\scriptsize{$\overline{DNS.1}$}} \UnaryInfC{$\lnot A, (A \to B) \to B \nvdash B$} \AxiomC{} \RightLabel{\scriptsize{\emph{Ax.}}} \UnaryInfC{$A \vdash A$} \RightLabel{\scriptsize{$L\lnot$}} \UnaryInfC{$\lnot A, A \vdash$} \RightLabel{\scriptsize{DNS.2}} \UnaryInfC{$\lnot A, (A \to B) \to B \vdash B$} \BinaryInfC{$\bot$} \end{prooftree}Therefore, \eqref{claim1} cannot be maintained in \(\mathbb{C}\) without contradiction: if Core logic is consistent, it cannot be paraconsistent. \(\blacksquare\)
2. Corollary
Tennant claims that this second antisequent
\begin{equation} \label{claim2} \tag{Claim 2} \lnot A, A \nvdash \lnot B \end{equation}is also true in Core logic, by contrast with M, which explains that in the Figure of logical system inclusions [1, p. 35] Tennant draws an overlap of \(\mathbb{C}\) on M. But, this is a mistake, because such a claim entails the same inconsistency, hence this corollary of the previous theorem:
\eqref{claim2} is false, therefore it cannot establish correctly that \(\mathbb{C}\) overlaps minimal logic.
Proof. \eqref{claim2} meets exactly the same contradiction:
\begin{prooftree} \AxiomC{} \RightLabel{\scriptsize{(Claim 2)}} \UnaryInfC{$\lnot A, A \nvdash \lnot B$} \RightLabel{\scriptsize{$\overline{DNS.1}$}} \UnaryInfC{$\lnot A, (A \to \lnot B) \to \lnot B \nvdash \lnot B$} \AxiomC{} \RightLabel{\scriptsize{\emph{Ax.}}} \UnaryInfC{$A \vdash A$} \RightLabel{\scriptsize{$L\lnot$}} \UnaryInfC{$\lnot A, A \vdash$} \RightLabel{\scriptsize{DNS.2}} \UnaryInfC{$\lnot A, (A \to \lnot B) \to \lnot B \vdash \lnot B$} \BinaryInfC{$\bot$} \end{prooftree}Therefore, \eqref{claim2} is false and cannot establish correctly that \(\mathbb{C}\) overlaps minimal logic. \(\blacksquare\)
3. Certification
The Theorem and its Corollary share the same certification in
These certifications differ in their logical foundations, and that
difference is precisely their joint interest. The Coq script is the
reference version: built on dependent type theory, it proves the
invertibility of DNS.1 by structural induction on derivations in
\(\mathcal{F}\), and its Print Assumptions command makes its whole
axiomatic basis auditable — it reports exactly the two principles the
argument grants to Tennant, with nothing else assumed. The Lean 4
file is a port of that script into another kernel of the same
type-theoretic family; written in pure core Lean 4, without any
Mathlib dependency, it can be re-checked in the browser at the link
above, with nothing to install. Athena, by contrast, rests on a
different paradigm altogether: a denotational proof language over
many-sorted first-order logic, driven by automated provers rather than
by a type-theoretic kernel. That the same contradiction is certified
in two dependent type theories and in a first-order denotational
language shows that this proof owes nothing to the idiosyncrasies of a
single system: it is the logical result of the conjunction of the
small fragment \(\mathcal{F}\) of \(\mathbb{C}\) and \eqref{claim1},
not an artefact of a specific formalism. The three source files are
available on GitHub.
4. References
