Explosion and Cut Required

[Joseph Vidal-Rosset]

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