# Explosion and Cut Required

Joseph Vidal-Rosset joseph.vidal.rosset at gmail.com
Thu Jun 2 06:04:58 EDT 2022

```> ------- Original Message -------
> Le mardi 31 mai 2022 à 02:39, Harvey Friedman <hmflogic at gmail.com> a écrit :
> In particular, I am seeking any FOM readers who can elucidate just what Tennant is claiming.
> Harvey Friedman

Hello Harvey, hello everyone,

Unfortunately, Neil Tennant did not reply in this thread on the list.

If I understand correctly the section 6.4.1 "Cut as a structural rule",
p. 150 of Core logic, OUP, 2017, does *not* deny the complexity theorem
according to which giving up the Cut rule (i.e. all lemmas) in
mathematical proofs would increase the complexity of mathematical proofs
dramatically.

But it is well known that the famous Cut elimination theorem is
important for its logical consequences, among them the theorem of
subformula property and the consistency theorem according to which "only
an inconsistent logical system S prove the void sequent via the Cut
rule, therefore, if S is consistent, all formulas S-provable are such
without the use of Cut rule". It is therefore widely admitted now that
"once a system is shown to have a cut elimination theorem, it is
normally immediate that the system is consistent."

Now, there is an intriguing problem with the treatment of the Cut rule
by the Core logician.

First, the *unrestricted Cut* must be ruled out from Core logic, just
because its use allows the derivation of the unwelcome "First Lewis's
Paradox". See p. 196 of Core logic for this couple of examples for which
all premises are provable in Core logic:

A: A v B    ¬A, A v B: B
------------------------ Cut
A, ¬A : B

¬A: A -> B      A, A -> B: B
----------------------------- Cut
¬A, A: B

To solve this difficulty, Neil Tennant replied that only a *restricted
Cut* is admissible and invented a new Cut rule, where cutting is needed
not only on the left, but also on the right, if and only if the premises
are jointly inconsistent. Let us call this Cut the "Core Cut", therefore
we have this admissible application of Core Cut where the derivation of
the First Lewis Paradox is avoided:

A: A v B    ¬A, A v B: B
------------------------- Cut
A, ¬A :

¬A: A -> B      A, A -> B: B
----------------------------- Cut
¬A, A:

According to Tennant, "There is no principled reason to confine the
potential ‘subsetting down’ to the left of the target sequent" (Core
logic, p. 155).

But I am afraid that, on the contrary, there are very good reasons to
reject this the "Core Cut" rule that can cut not only on the left, but
also on the right, if the set of premises is inconsistent. One of them
is that the Cut elimination theorem is based on the presupposition that
*nothing must be said*, in Gentzen's proof, on the consistency or the
inconsistency of the set of premises. I point out that Gentzen's proof
of Cut elimination theorem also shows that only an inconsistent set of
premises can deduce any atomic formula, if I have correctly understood
Dummett, who wrote ("Elements of Intuitionism", 4.3 "Cut Elimination",
p. 105) :

> Cut-elimination is directly connected with establishing consistency, and was
> so intended by Gentzen. Given the equivalence of N and L [i.e. natural deduction and sequent calculus], acceptance of ex
> falso quodlibet in the form of  ¬ - in N or thinning on the right in L makes the
> consistency of N equivalent to the non-derivability of the empty sequent '0 : 0'
> in L. But simply by examination of the rules of L, it is clear that there is no
> rule by which this sequent could possibly be derived. *Recognition of ¬ - [i.e. the intutionistic absurdity rule] as a
> correct principle thus amounts to recognizing the consistency of N.* [I emphasize].

If the Core logician contests Dummett's point, then he has to provide an
Cut elimination theorem, of course, independent of Gentzen's, where the
Core Cut rule will be used. But because the Core Cut rule means cut only
the left when premises are consistent, by contrast with cut on the left
and on the right, in the case of inconsistency of premises, I do not see
what such an independent Cut elimination theorem for Core logic can
really prove.

Best wishes,

Jo.

```