Core Inconsistency

2021-03-03, updated 2021-03-03 next - previous

This note provides a very simple proof that three claims about Core logic (i.e. Tennant’s logic) are jointly incompatible. Comments are welcome.

According to Tennant,

  1. Core logic is paraconsistent [1, p. 15]; therefore

    \begin{equation} \label{para} \lnot A, A \nvdash B \end{equation}
  2. Core logic is intuitionistic insofar as any theorem of intuitionistic logic is Core provable [1, p. 43]; therefore axiom X of Heyting’s propositional logic [2, p. 102] that is

    \begin{equation} \label{heyting} \vdash \lnot A \to (A \to B) \end{equation}

    is a Core theorem.

  3. Core logic is respectful of truth tables. About this last point,Tennant wrote p. [1, p. 185]:

One insists also on vindicating the truth tables for the connectives.

The conjunction of claims 1, 2 and 3 entails a contradiction.

The following sequent and the couple of theorems are all provable in Core logic:

\begin{equation} \label{fatal2} \lnot A , A \vdash (\lnot A \to (A \to B)) \to B \end{equation} \begin{prooftree} \AxiomC{$\scriptsize{1}$} \noLine \UnaryInfC{$\lnot A \to (A \to B)$} \AxiomC{$\lnot A$} \AxiomC{$\scriptsize{2}$} \noLine \UnaryInfC{$A \to B$} \AxiomC{$A$} \AxiomC{$\scriptsize{3}$} \noLine \UnaryInfC{$B$} \RightLabel{$\scriptsize{\to E,3}$} \TrinaryInfC{$B$} \RightLabel{$\scriptsize{\to E, 2}$} \TrinaryInfC{$B$} \RightLabel{$\scriptsize{\to_{b} I, 1}$} \UnaryInfC{$(\lnot A \to (A \to B)) \to B$} \end{prooftree}

\begin{equation} \label{reduc} \vdash ((\lnot A \to (A \to B)) \to B) \to B \end{equation} \begin{prooftree} \AxiomC{$\scriptsize{1}$} \noLine \UnaryInfC{$(\lnot A \to (A \to B)) \to B$} \AxiomC{$\scriptsize{2}$} \noLine \UnaryInfC{$\lnot A$} \AxiomC{$\scriptsize{3}$} \noLine \UnaryInfC{$A$} \RightLabel{$\scriptsize{\lnot E}$} \BinaryInfC{$\bot$} \RightLabel{$\scriptsize{\to_{a} I, 3}$} \UnaryInfC{$A \to B$} \RightLabel{$\scriptsize{\to_{b} I, 2}$} \UnaryInfC{$\lnot A \to (A \to B)$} \AxiomC{$\scriptsize{4}$} \noLine \UnaryInfC{$B$} \RightLabel{$\scriptsize{\to E, 4}$} \TrinaryInfC{$B$} \RightLabel{$\scriptsize{\to_{b} I, 1}$} \UnaryInfC{$((\lnot A \to (A \to B)) \to B) \to B$} \end{prooftree}

\begin{equation} \label{complic} \vdash B \to ((\lnot A \to (A \to B)) \to B) \end{equation} \begin{prooftree} \AxiomC{$\scriptsize{1}$} \noLine \UnaryInfC{$B$} \RightLabel{$\scriptsize{\to_{b} I}$} \UnaryInfC{$(\lnot A \to (A \to B)) \to B$} \RightLabel{$\scriptsize{\to_{b} I, 1}$} \UnaryInfC{$B \to ((\lnot A \to (A \to B)) \to B)$} \end{prooftree}

The last two syntactic deductions above prove that

\begin{equation} \label{con} (\lnot A \to (A \to B)) \to B \end{equation}


\begin{equation} \label{atom} B \end{equation}

are logically equivalent in Core logic. As theorem, \eqref{reduc} means that, quite independently of any set of undischarged assumptions (that is independently of any context), \eqref{con} is always reducible to \eqref{atom}, while theorem \eqref{complic} shows in turn that \eqref{atom} can always be perversely hidden behind \eqref{con}.

Note that, because of theorem \eqref{heyting}, the semantic proof that \eqref{con} is reducible to \eqref{atom} is trivial thanks to rule (v) of Quine’s algorithm [3, p. 14]:

Drop \(\top\) as antecedent of a conditional. (Reason: a conditional with true antecedent is true or false according as the consequent is true or false).

Quine’s rule (v) should be admissible in Core logic on the base of the third claim for Core logic, as in any logical system which respects truth tables, this rule being based on an inspection of the truth table for the conditional. Thus, on the right of sequent \eqref{fatal2}, Quine’s rule (v) allows the reduction of conditional \eqref{con} to its only consequent, that is to atom \eqref{atom}, for the reason that the antecedent of conditional \eqref{con} i.e. \eqref{heyting} is a Core theorem and is true by definition.

Therefore, to conclude in the style of Wittgenstein [4], sequent \eqref{fatal2} in Core logic says that

\begin{equation} \label{LFP} \lnot A, A \vdash B \end{equation}

syntactically as well as semantically, and this logical fact is in contradiction with the first claim for Core logic expressed by formula \eqref{para}.

All the usual objections against the derivation of Lewis’s First Paradox are avoided by the proof above:

  1. All deductions that lead to the conclusion are in normal form, as requested by the Core logician.
  2. There is no use of the Cut rule, because the proof above focuses only the right of the turnstile, not on its left.

The right way of understanding the proof above is the following reasoning based on the difference between minimal logic and intuitionistic logic: sequent \eqref{fatal2} is provable in minimal logic, but the conditional on its right of has an antecedent i.e. \eqref{heyting} which is a proper assumption, that is an assumption that is not derivable in this logical system, according to the definition given by Negri and von Plato [5, pp. 8.5.5., 201]. By contrast, in intuitionistic logic as well as in Core logic, \eqref{heyting} is intuitionistically provable and that is the reason why the equivalence of \eqref{con} and \eqref{atom} is an intuitionistic theorem and therefore also a Core theorem:

\begin{equation} \label{equiv} \vdash ((\lnot A \to (A \to B)) \to B) \leftrightarrow B \end{equation}

Formula \eqref{equiv} is valid whatever the context, in other words, it would be inconsistent to deny that the following Weakening on the left is admissible, even in Core logic:

\begin{prooftree} \AxiomC{$\vdash ((\lnot A \to (A \to B)) \to B) \leftrightarrow B$} \RightLabel{$\scriptsize{LW}$} \UnaryInfC{$\Delta \vdash ((\lnot A \to (A \to B)) \to B) \leftrightarrow B$} \end{prooftree}

Replace \((\lnot A \to (A \to B)) \to B) \leftrightarrow B\) by \(\top\).

To sum up:

This proof is based on the fact that the Core proof of \eqref{fatal2} hides an abnormality. First, let us recall Prawitz’s inversion principle [6, pp. 33–34]:

\([\dots]\) nothing is “gained” by inferring a formula through introduction for use as a major premiss in an elimination.

This basic principle which founds normalization in natural deduction is ignored by Core logic, where a second rule for conditional introduction replaces the intuitionistic rule of elimination of the absurdity constant. Then, the sleight of hand is to demand that all evidence be in normal form, a clearly arbitrary request when the inversion principle is carefully glossed over. If rule \(\bot E\) is replaced by rule \(\to_{a} I\) and if all Core proofs must be in normal form, then it is not surprising that rule \(\bot E\) is not derivable in Core logic: it is contained in the introduction rule \(\to_{a} I\) to prove all intuitionistic theorems that needed rule \(\bot E\) and, because rule \(\bot E\) is suppressed, no normal proof can deduce a sequent where an atom is deduced from \(\bot\) “at the level of the turnstile”.

Nevertheless, Core logic hides at least one abnormality in one its proofs where it is possible to see the deduction of Lewis’s First Paradox. Indeed, note that the proof of sequent \eqref{fatal2} contains theorem \eqref{heyting} as major premiss. According to theorem 8.5.6 published by Negri and von Plato [5, p. 201], “given a derivation, there is a derivation in which all major premisses of elimination rules are proper assumptions [that is to say an underivable assumption as major premiss of an elimination rule]”. This theorem is one of the logical consequences of Prawitz’s inversion principle: its proof involves normalization. Therefore, it must be conceded that in the main part of the Core proof of sequent \eqref{fatal2} there is an hidden abnormality highlighted by the following deduction which shows that the major premiss is not a proper assumption:

\begin{prooftree} \AxiomC{$\scriptsize{1}$} \noLine \UnaryInfC{$\lnot A$} \AxiomC{$\scriptsize{2}$} \noLine \UnaryInfC{$A$} \RightLabel{$\scriptsize{\lnot E}$} \BinaryInfC{$\bot$} \RightLabel{$\scriptsize{\to_{a} I, 2}$} \UnaryInfC{$A \to B$} \RightLabel{$\scriptsize{\to_{b} I, 1}$} \UnaryInfC{$\lnot A \to (A \to B)$} \AxiomC{$\lnot A$} \AxiomC{$\scriptsize{3}$} \noLine \UnaryInfC{$A \to B$} \AxiomC{$A$} \AxiomC{$\scriptsize{4}$} \noLine \UnaryInfC{$B$} \RightLabel{$\scriptsize{\to E,4}$} \TrinaryInfC{$B$} \RightLabel{$\scriptsize{\to E, 3}$} \TrinaryInfC{$B$} \end{prooftree}

Now, focusing only on the undischarged assumptions and the conclusion of the deduction above, everyone can see that sequent \eqref{LFP} is proved:

\begin{prooftree} \AxiomC{$\lnot A$} \AxiomC{$A$} \BinaryInfC{$B$} \end{prooftree}

in contradiction with \eqref{para}.

The way out for Tennant is then to claim that the normalization of the abnormal proof above does not lead to conclude nothing but \(\bot\), and it is, according to Tennant, an “epistemic gain” to learn that from an inconsistent set of premises, nothing is deducible, except a contradiction mark. The trouble is that this new “normalization” corresponds to any known conversion rule to natural deduction, because all conversions known for the normalization of proofs end always on a conclusion that is the same as that of abnormal proof [7, pp. 23–29]. Last, whether throwing overboard the intuitionistic absurdity rule is really an “epistemic gain” is still an open question. Contrarily to what is claimed by philosophers and logicians who are seduced by paraconsistency, it can be an epistemic gain to know that from contradiction any sentence is deducible, and if there are good reasons to keep this rule, it is a epistemic loss than to reject it.


N. Tennant, Core Logic, 1st ed. Oxford University Press, 2017 [Online]. Available:
A. Heyting, Intuitionism: An Introduction, 2nd ed. North Holland Publishing Company, 1956.
W. v. O. Quine, Methods of Logic. Cambridge, Mass., U.S.A.: Harvard University Press, 1982.
L. Wittgentstein, Tractatus Logico-Philosophicus. Sweden: Chiron Academic Press, 2016 [Online]. Available:
S. Negri and J. von Plato, Structural Proof Theory. Cambridge: Cambridge University Press, 2001.
D. Prawitz, Natural Deduction - A Proof Theoretical Study. Uppsala: Almqvist & Wilksell, 1965.
S. Negri and J. v. Plato, Proof Analysis: A Contribution to Hilbert’s Last Problem. Cambridge, U.K., U.S.A., 2011.

Made with Emacs 27.1 (Org mode 9.4.4) 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