# Paraconsistent, Tennant’s Logic Is Inconsistent

2022-06-10, updated 2022-07-29 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 *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} |

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.

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

The Cut rule is *admissible* in Core logic [3, pp. 16–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}or

\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

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

and

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

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.

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

*Logical Options: an Introduction to Classical and Alternative Logics*. Peterborough, Ont., Canada: Broadview Press, 2001.