Paraconsistent, Tennant’s Logic Is Inconsistent

2022-06-10, updated 2022-06-23 next - previous

The claim according to which the First Lewis’s Paradox is unprovable in Tennant’s logical system (i.e. Core logic) entails a contradiction in this system and therefore makes it inconsistent.

A logical system S is said “paraconsistent” if and only if

\begin{equation} \label{eq:1} \lnot A, A \vdash B \end{equation}

is invalid in S, that is to say, if in S

\begin{equation} \label{eq:2} \lnot A, A \nvdash B \end{equation}

A theory \(\mathcal{T}\) is inconsistent if and only if a contradiction is derivable from \(\mathcal{T}\), using the logical system of \(\mathcal{T}\) and its claims, that is to say, if and only if \[ \mathcal{T} \vdash \bot \] (See and [1] p. 80.)

A rule is derivable in a given system of rules, if its conclusion is derivable from its premisses in the system [2] (p. 47).

\(\label{eq:89}\) A rule is admissible in a given system of rules if its conclusion is derivable in the system whenever its premisses are. [2] (p. 47).

The logical system invented by Tennant and called “Core logic” is defined as a subsystem of classical logic and claimed to be paraconsistent [3] (p. 156).

Antisequent \eqref{eq:2} cannot be claimed in Core logic without making Core logic inconsistent; in other words, if Core logic is paraconsistent, then it is inconsistent.

The proof of this theorem is going to be given in the sequent calculus for propositional Core logic [3] (pp. 161-163) whose rules are in the Table below:


1- The following rules that I call “the rules of Double Negation à la Slaney” [4] i.e. \(\scriptsize{DNS.1}\), \(\scriptsize{DNS.2}\), \(\scriptsize{DNS.3}\):

\begin{prooftree}\AxiomC{$ \Delta, \varphi \vdash \psi$}\RightLabel{\(\scriptsize{ DNS.1}\)} \UnaryInfC{$\Delta, (\varphi \to \psi) \to \psi \vdash \psi$}\end{prooftree} \begin{prooftree}\AxiomC{$ \Delta, \varphi \vdash $}\RightLabel{\(\scriptsize{DNS.2}\)} \UnaryInfC{$\Delta, \lnot \lnot \varphi \vdash $} \end{prooftree}
\begin{prooftree} \AxiomC{$ \Delta, \varphi \vdash $} \RightLabel{$\scriptsize{DNS.3}$} \UnaryInfC{$\Delta, (\varphi \to \psi) \to \psi \vdash \psi$} \end{prooftree}

are all derivable in Core logic.

2- If Core logic is consistent, the following derivability relations between antisequents that I call, to follow Goranko [5] , \(\scriptsize{\overline{DNS.1}}\) i.e.

\begin{prooftree} \AxiomC{$ \Delta, \varphi \nvdash \psi$} \RightLabel{$\scriptsize{\overline{DNS.1}}$} \UnaryInfC{$\Delta, (\varphi \to \psi) \to \psi \nvdash \psi$} \end{prooftree}

is a logical consequence of \(\scriptsize{DNS.1}\). To prove it, first, let us show that \(\scriptsize{DNS.1}\) is invertible:

\begin{prooftree} \AxiomC{} \RightLabel{$\scriptsize{Ax.}$} \UnaryInfC{$\varphi \vdash \varphi$} \AxiomC{} \RightLabel{$\scriptsize{Ax.}$} \UnaryInfC{$\psi \vdash \psi$} \RightLabel{$\scriptsize{L\to}$} \BinaryInfC{$\varphi, \varphi \to \psi \vdash \psi$} \RightLabel{$\scriptsize{R\to}$} \UnaryInfC{$\varphi \vdash (\varphi \to \psi) \to \psi$} \AxiomC{$\Delta, \varphi \vdash \psi $} \RightLabel{$\scriptsize{R \to}$} \UnaryInfC{$\Delta \vdash \varphi \to \psi$} \AxiomC{} \RightLabel{$\scriptsize{Ax.}$} \UnaryInfC{$\psi \vdash \psi$} \RightLabel{$\scriptsize{L\to}$} \BinaryInfC{$ \Delta, (\varphi \to \psi) \to \psi \vdash \psi$} \RightLabel{$\scriptsize{Cut}$} \BinaryInfC{$\Delta, \varphi \vdash \psi $} \end{prooftree}

The Cut rule is admissible in Core logic [3] (pp. 16, 37-39, 152-156). According to the definition of the admissibility of a rule given above, it means that, whenever it is provable that \(\Delta, \varphi \vdash \psi\), it is provable that \(\Delta, (\varphi \to \psi) \to \psi \vdash \psi\), and conversly, via Cut, it is provable in that \(\Delta, \varphi \vdash \psi\).

Now, it is provable that

\begin{prooftree} \AxiomC{$\Delta, \varphi \nvdash \psi$} \RightLabel{$ \scriptsize{\overline{DNS.1}}$} \UnaryInfC{$\Delta, (\varphi \to \psi) \to \psi \nvdash \psi$} \end{prooftree}

is a logical consequence of \(\scriptsize{DNS.1}\), because, if it was not the case, then either

\begin{prooftree} \AxiomC{$ \Delta, \varphi \nvdash \psi$} \UnaryInfC{$\Delta, (\varphi \to \psi) \to \psi \vdash \psi$} \end{prooftree}


\begin{prooftree} \AxiomC{$ \Delta, \varphi \vdash \psi$} \UnaryInfC{$\Delta, (\varphi \to \psi) \to \psi \nvdash \psi$} \end{prooftree}

could be satisfiable in Core logic, in contradiction with the invertibility of \(\scriptsize{DNS.1}\) that just has been shown. Therefore, if Core logic is consistent, \(\scriptsize{\overline{DNS.1}}\) is a logical consequence of \(\scriptsize{DNS.1}\).

This point can also be proved via the invertibility of \(\scriptsize{DNS.1}\) and the propositional Core logic. Indeed, the following sequent

\begin{equation} \label{eq:3} A \leftrightarrow B \vdash \lnot A \leftrightarrow \lnot B \end{equation}


\begin{equation} \label{bisinterderiv} A \to B, B \to A \vdash (\lnot B \to \lnot A) \land (\lnot A \to \lnot B) \end{equation}

is provable in Core logic as follows

\begin{prooftree} \AxiomC{} \RightLabel{$\scriptsize{Ax.}$} \UnaryInfC{$A \vdash A$} \AxiomC{} \RightLabel{$\scriptsize{Ax.}$} \UnaryInfC{$B \vdash B$} \RightLabel{$\scriptsize{L \lnot}$} \UnaryInfC{$\lnot B, B \vdash $} \RightLabel{$\scriptsize{L\to}$} \BinaryInfC{$A, \lnot B, A \to B \vdash $} \RightLabel{$\scriptsize{R\lnot}$} \UnaryInfC{$\lnot B, A \to B \vdash \lnot A$} \RightLabel{$\scriptsize{R\to}$} \UnaryInfC{$A \to B \vdash \lnot B \to \lnot A$} \AxiomC{} \RightLabel{$\scriptsize{Ax.}$} \UnaryInfC{$B \vdash B$ } \AxiomC{} \RightLabel{$\scriptsize{Ax.}$} \UnaryInfC{$A \vdash A$} \RightLabel{$\scriptsize{L \lnot}$} \UnaryInfC{$\lnot A, A \vdash $} \RightLabel{$\scriptsize{L\to}$} \BinaryInfC{$B, \lnot A, B \to A \vdash $} \RightLabel{$\scriptsize{R\lnot}$} \UnaryInfC{$\lnot A, B \to A \vdash \lnot B$} \RightLabel{$\scriptsize{R\to}$} \UnaryInfC{$B \to A \vdash \lnot A \to \lnot B$} \RightLabel{$\scriptsize{R\land}$} \BinaryInfC{$ A \to B, B \to A \vdash (\lnot B \to \lnot A) \land (\lnot A \to \lnot B)$} \end{prooftree}

if \(A\), \(B\), \(\lnot A\) and \(\lnot B\) stand for respectively the sequents and antisequents of \(\scriptsize{DNS.1}\) and \(\scriptsize{\overline{DNS.1}}\) rules, the proof of \eqref{eq:3}. In other words, each interderivability between sequent A in the premiss of \(\scriptsize{DNS.1}\) rule and sequent B in the conclusion of the same rule entails in turn an interderivability between the corresponding antisequents \(\lnot A\) and \(\lnot B\). For example, \(\scriptsize{DNS.1}\) is an invertible rule that says that \[\Delta, \varphi \vdash \psi ~~ \Leftrightarrow ~~ \Delta, (\varphi \to \psi) \to \psi \vdash \psi\] therefore, \(\scriptsize{\overline{DNS.1}}\) is deducible and must be also invertible: \[\Delta, \varphi \nvdash \psi ~~ \Leftrightarrow ~~ \Delta, (\varphi \to \psi) \to \psi \nvdash \psi\] If it was not the case, then \eqref{eq:3} would be falsifiable, which is impossible. Consequently, it would be absurd that the interderivability expressed by the invertible \(\scriptsize{DNS.1}\) rules would not entail in Core logic the deducibility relations between their respective antisequents in \(\scriptsize{\overline{DNS.1}}\) rule.

The objection that would probably not fail to come to the mind of the Core logician would be to refuse that \(\scriptsize{DNS.1}\) rule imply the validity of \(\scriptsize{\overline{DNS.1}}\) rule in Core logic, that he can for example both affirm \(\scriptsize{DNS.1}\) and challenge the claim according to which this derivable rule entails \(\scriptsize{\overline{DNS.1}}\). If the Core logician would be right, \(\scriptsize{\overline{DNS.1}}\) could stay as not asserted in Core logic. But this line of defense leads to a contradiction. Indeed, \eqref{eq:3} is of course also provable via the trees method for propositional intuitionistic logic [6] . It means that there is an intuitionistic proof that shows syntactically the contradiction in the conjunction of claims

\begin{equation} \label{eq:5} A \leftrightarrow B \end{equation}


\begin{equation} \label{eq:6} ?(\lnot B \leftrightarrow \lnot A) \end{equation}

where symbol “?” means that \(\lnot B \leftrightarrow \lnot A\) is not asserted. The proof is left to the reader, who can also copy the formula below

(a <=> b) => (~b <=> ~a)

to paste it as input for FCube-prover. The efficient refutation method of this intuitionistic prover shows that this formula is intuitionistically provable, because it cannot be considered without contradiction as not known to be true, that is to say as false at one possible step of development knowledge.

Therefore, if Core logic is consistent, \(\scriptsize{DNS.1}\) entails \(\scriptsize{\overline{DNS.1}}\) and this rule for antisequents must be considered as valid in Core logic.

3- Last, it is now provable that if \(\{\Delta, \varphi\}\) is a set of contradictory assumptions, then it is inconsistent in Core logic to claim that no atomic formula is deducible from such a set:

\begin{prooftree} \AxiomC{$ \Delta, \varphi \nvdash \psi$} \RightLabel{$\scriptsize{\overline{DNS.1}}$} \UnaryInfC{$\Delta, (\varphi \to \psi) \to \psi \nvdash \psi$} \AxiomC{$\Delta, \varphi \vdash $} \RightLabel{$\scriptsize{DNS.3}$} \UnaryInfC{$ \Delta, (\varphi \to \psi) \to \psi \vdash \psi$} \BinaryInfC{$\bot$} \end{prooftree}

Replacing respectively \(\Delta\), \(\varphi\) and \(\psi \) by \(\lnot A\), \(A\) and \(B\), one gets:

\begin{prooftree} \AxiomC{$ \lnot A, A \nvdash B$} \RightLabel{$\scriptsize{\overline{DNS.1}}$} \UnaryInfC{$\lnot A, (A \to B) \to B \nvdash B$} \AxiomC{$\lnot A, A \vdash $} \RightLabel{$\scriptsize{DNS.3}$} \UnaryInfC{$ \lnot A, (A \to B) \to B \vdash B$} \BinaryInfC{$\bot$} \end{prooftree}

Therefore, antisequent \eqref{eq:2} cannot be claimed in Core logic without making Core logic inconsistent. Johansson claims for minimal logic only the premiss on the left, Heyting claims for intuitionistic logic only the premiss on the right, Tennant claims both for Core logic, hence the inconsistency of Core logic, if this system is claimed to be paraconsistent.

David, R. et al.: Introduction à la logique: théorie de la démonstration. Paris: Dunod, 2004.
von Plato, J.: Elements of Logical Reasoning. Cambridge University Press, 2013.
Tennant, N.: Core Logic. Oxford University Press, 2017.
Slaney, J.: Minlog. 1994.
Bell, J. et al.: Logical Options: an Introduction to Classical and Alternative Logics. Peterborough, Ont., Canada: Broadview Press, 2001.

Made with Emacs 29.0.50 (Org mode 9.5) and with org-export-head, a blog exporter.

The css file of this blog is mainly the result of Zhitao Gong's work.

orgmode emacs isso debian mxlinux