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

*paraconsistent*[1, p. 15]; therefore \begin{equation} \label{para} \lnot A, A \nvdash B \end{equation}*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.

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

The last two syntactic deductions above prove that

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

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

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:

- All deductions that lead to the conclusion are in normal form, as requested by the Core logician.
- 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:

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:

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

To sum up:

- in minimal logic, the provability of \eqref{fatal2} is consistent with the unprovability of \eqref{equiv} and \eqref{LFP};
- \eqref{fatal2} , \eqref{equiv}, \eqref{LFP} are consistently provable in intuitionistic logic;
in Core logic, \eqref{fatal2} and \eqref{equiv} are provable, but,

\begin{prooftree} \AxiomC{$\lnot A, A \vdash (\lnot A \to (A \to B)) \to B$} \AxiomC{$\vdash ((\lnot A \to (A \to B)) \to B) \leftrightarrow B$} \AxiomC{$\lnot A, A \nvdash B$} \TrinaryInfC{$\bot$} \end{prooftree}*inconsistently*, \eqref{LFP} is claimed to be unprovable in Core logic, i.e.

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:

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.

## Bibliography

*Core Logic*, 1st ed. Oxford University Press, 2017 [Online]. Available: https://global.oup.com/academic/product/core-logic-9780198777892?cc=fr&lang=en&

*Tractatus Logico-Philosophicus*. Sweden: Chiron Academic Press, 2016 [Online]. Available: https://www.wisehouse-publishing.com