Core Inconsistency

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

This note provides a very simple proof that at least two 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 also provable in Core logic [1, p. 43]. Consequently, axiom X of Heyting’s propositional logic [2, p. 102] which is

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

    is a theorem in Core logic.

Core logic is inconsistent, because the conjunction of claims 1 and 2 entails a contradiction.

Sequent \eqref{fatal2} and theorems \eqref{reduc} and \eqref{complic} are provable in Core logic as follows:

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

From \eqref{reduc}, \eqref{fatal2} and \eqref{para}, a contradiction is derivable i.e.

\begin{prooftree} \AxiomC{$\vdash ((\lnot A \to (A \to B)) \to B) \to B$} \AxiomC{$\lnot A, A \vdash (\lnot A \to (A \to B)) \to B$} \AxiomC{$\lnot A, A \nvdash B$} \TrinaryInfC{$\bot$} \end{prooftree}

Indeed, from \eqref{reduc} and \eqref{fatal2} it is possible to deduce Lewis’s First Paradox in Core logic as follows:

\begin{prooftree} \AxiomC{$((\lnot A \to (A \to B)) \to B) \to B$} \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$} \AxiomC{$\scriptsize{4}$} \noLine \UnaryInfC{$B$} \RightLabel{$\scriptsize{\to E, 4}$} \TrinaryInfC{$B$} \end{prooftree}

The proof of theorem \eqref{reduc} shows that the inference

\begin{prooftree} \AxiomC{$(\lnot A \to (A \to B)) \to B$} \UnaryInfC{$B$} \end{prooftree}

is provable in Core logic, therefore the deduction above is reducible to

\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$} \UnaryInfC{$B$} \end{prooftree}

that is to say, by keeping only the undischarged assumptions:

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

in contradiction with \eqref{para}.

Tennant claims that truth tables are respected by Core logic [1, p. 185], but it is false that his system respects truth tables as method of logic.

Note that, because of theorem \eqref{heyting}, the semantic proof that \eqref{con} is reducible to \eqref{atom} should be 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 claim that Core logic respects truth tables: as in any logical system respectful of 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], in contradiction with the first claim for Core logic expressed by formula \eqref{para}, sequent \eqref{fatal2} in Core logic says that

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

because \eqref{con} and \eqref{atom} are semantically identical: both are true or false depending exclusively on the truth or falsity of B. But in spite of their equivalence, the Core logician denies that \eqref{atom} can replace \eqref{con} on the right of sequent \eqref{fatal2}, therefore it is false that Core logic respects truth tables as method of logic.


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:

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