# 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

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

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 \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-

\begin{prooftree} \AxiomC{$ \Delta, \varphi \nvdash \psi$} \RightLabel{$\scriptsize{\overline{DNS.1}}$} \UnaryInfC{$\Delta, (\varphi \to \psi) \to \psi \nvdash \psi$} \end{prooftree}*If Core logic is consistent*, the following derivability relations between antisequents that I call, to follow Goranko [5], \(\scriptsize{\overline{DNS.1}}\) i.e.

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

i.e.

\begin{equation} \label{eq:9} \Delta, \varphi \vdash \bot \end{equation}
is provable (*resp.* unprovable) *if and only if*

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:

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}\):

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:

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:

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:

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.

*Introduction à la logique: théorie de la démonstration*. Paris: Dunod, 2004.