Paraconsistent, Tennant’s Logic Is Inconsistent
2022-06-10, updated 2024-04-09 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 The consistency of inconsistency claims 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 called invertible in a sequent calculus system if a proof of its conclusion implies the existence of proofs of each of its premises.
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].
\(\Delta, \varphi \nvdash \psi\) is an antisequent and means \(\lnot(\Delta, \varphi \vdash \psi)\) i.e. that \(\psi\) is not derivable from \(\{\Delta, \varphi\}\).
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 three steps, in the language of sequent calculus for propositional Core logic [3, pp. 161–163] whose rules are in the Table below:
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 $} \RightLabel{$\scriptsize{DNS.3}$} \UnaryInfC{$\Delta, (\varphi \to \psi) \to \psi \vdash \psi$} \end{prooftree}\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} are all derivable in Core logic.
\(\scriptsize{DNS.1}\) is derivable:
\begin{prooftree} \AxiomC{$\Delta, \varphi \vdash \psi $} \RightLabel{$\scriptsize{R_{b} \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$} \end{prooftree}\(\scriptsize{DNS.2}\) is derivable:
\begin{prooftree} \AxiomC{$\Delta, \varphi \vdash$} \RightLabel{$\scriptsize{R \lnot}$} \UnaryInfC{$\Delta \vdash \lnot \varphi$} \RightLabel{$\scriptsize{L\lnot }$} \UnaryInfC{$ \Delta, \lnot \lnot \varphi \vdash $} \end{prooftree}\(\scriptsize{DNS.3}\) is derivable:
\begin{prooftree} \AxiomC{$\Delta, \varphi \vdash $} \RightLabel{$\scriptsize{R_{a} \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$} \end{prooftree}
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, let us show in a first time that \(\scriptsize{DNS.1}\) is invertible. The easiest way of proving the invertibility of \(\scriptsize{DNS.1}\) is to point out that \(\scriptsize{DNS.2}\) is also invertible, and that it is only a particular case of \(\scriptsize{DNS.1}\). Indeed, \(\scriptsize{DNS.2}\) is an invertible rule because
\begin{equation} \label{eq:14} \Delta, \varphi \vdash \end{equation}i.e.
\begin{equation} \label{eq:9} \Delta, \varphi \vdash \bot \end{equation}is provable (resp. unprovable) if and only if
\begin{equation} \label{eq:13} \Delta, \lnot \lnot \varphi \vdash \end{equation}i.e.
\begin{equation} \label{eq:17} \Delta, (\varphi \to \bot) \to \bot \vdash \bot \end{equation}is also provable (resp. unprovable).
Rule \(\scriptsize{DNS.1}\) says the same thing: if a sequent whose form is
\begin{equation} \label{eq:3} \Delta, ( \dots ((((\varphi \to \psi) \to\psi) \to\psi) \to\psi) \dots) \to \psi \vdash \psi \end{equation}where the number of formulas expressed above by \(\psi\) is, on the left of the turnstile, an even number, then such a sequent can be reduced to case 0 (the first even number in \(\mathbb{N}\)), that is to say:
\begin{equation} \label{eq:4} \Delta, \varphi \vdash \psi \end{equation}and conversly any sequent of form \eqref{eq:4} implies a sequent of form \eqref{eq:3}, provided that the number of \(\psi\) in this form is, on the left of the turnstile, an even number. Therefore, by a structural induction on the proof tree based on a simple indefinite application of rule \(\scriptsize{DNS.1}\):
\begin{prooftree} \AxiomC{$\Delta, \varphi \vdash\psi$} \RightLabel{$\scriptsize{DNS.1}$} \UnaryInfC{$ \Delta, (\varphi \to\psi) \to\psi \vdash\psi$} \RightLabel{$\scriptsize{DNS.1}$} \UnaryInfC{$ \Delta, (((\varphi \to\psi) \to\psi) \to\psi) \to\psi \vdash\psi$} \RightLabel{$\scriptsize{DNS.1}$} \UnaryInfC{$ \Delta, (((((\varphi \to\psi) \to\psi) \to\psi) \to\psi) \to\psi) \to\psi \vdash\psi$} \UnaryInfC{$\vdots$}\end{prooftree}we see that the rule is trivially invertible (intuitively, we can always subtract what we had added, by following the reverse order):
\begin{prooftree} \AxiomC{$\vdots$} \UnaryInfC{$\Delta, (((((\varphi \to\psi) \to\psi) \to\psi) \to\psi) \to\psi) \to\psi \vdash\psi$} \UnaryInfC{$ \Delta, (((\varphi \to\psi) \to\psi) \to\psi) \to\psi \vdash\psi$} \UnaryInfC{$\Delta, (\varphi \to\psi) \to\psi \vdash\psi $} \UnaryInfC{$\Delta, \varphi \vdash \psi$} \end{prooftree}Once established the invertibilty \(\scriptsize{DNS.1}\), it is easy to prove via propositional Core logic that the following antisequent rule:
\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}\) The sequent
\begin{equation} \label{eq:5} A \leftrightarrow B \vdash \lnot A \leftrightarrow \lnot B \end{equation}i.e.
\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 valid in Core logic:
\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}and 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:5} proves that \(\scriptsize{\overline{DNS.1}}\) is a logical consequence of \(\scriptsize{DNS.1}\): the invertibility of rule \(\scriptsize{DNS.1}\) implies that its premiss is unprovable if and only if its conclusion is also unprovable.
3- Last, let us see 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 deduction on the left, Heyting claims for intuitionistic logic only the deduction on the right, Tennant claims both for Core logic, hence the inconsistency of Core logic, if this system is claimed to be paraconsistent.
But this contradiction can also be established as follows, without reference to any antisequent rule. On the one hand, the reader can check that the intuitionistically valid sequent
\begin{equation} \label{eq:7} \lnot A, (A \to B) \to B \vdash B \end{equation}is also provable in Core logic; therefore sequent \eqref{eq:1} should be provable in Core logic due to the invertibility of \(\scriptsize{DNS.1}\) which, proven by structural induction, admits by definition no counterexamples. That contradicts the claim that Core logic is a paraconsistent system. On the other hand, if that claim should be accepted, that is to say if \eqref{eq:2} would be true in Core logic, then \eqref{eq:7} should not be Core provable (that is also a logical consequence of the invertibility of \(\scriptsize{DNS.1}\)), but this is contradicted by the Core provability of \eqref{eq:7}. Consequently, if Core logic is claimed paraconsistent, then it is inconsistent.
