Explosion and Cut Required

[dennis.hamilton at acm.org]

> -----Original Message-----
> From: FOM <fom-bounces at cs.nyu.edu> On Behalf Of Joseph Vidal-Rosset
> Sent: Monday, June 13, 2022 00:14
> Subject: Re: Explosion and Cut Required


[orcmid] > Le 13/06/2022 à 00:36, Mario Carneiro a écrit :
[orcmid] [ ... ]

> ]I pointed out to you that this argument is valid in minimal logic, because 
> it is provable in minimal logic as in Core logic that

 > A -> B, B -> A |- (~B -> ~A) & (~A -> ~B)

 > Semantically, the above sequent is transparent: it says, if A is true if 
and only if B is also true (that is to say, A and B are equivalent), therefore 
B is false if and only if A is false. Let us replace A and B respectively by 
top (the truth constant) and ~bot (the negation of the absurdity constant), we 
have:

> top -> ~bot,  ~bot -> top |- (~ ~bot -> ~top) & (~top -> ~ ~ bot)

[ ... ]

This strikes me as sleight of hand.

The first deduction is consistent with the definition of bi-conditional, 
equivalence.  It is effectively by definition.

But arbitrary substitutions do not hold.  Substitutions of constants for A and 
B in *premises* do not work unless the premises remain sound.

I suggest that all you have shown is that the substitutions you make are 
unsound and cause inconsistency.

No surprise.

The same injuries arise from proffered deductions such as

A, ~A |- anything (including A & ~A)

when the law of excluded middle is axiomatic.

The parading of deduction schemes strikes me as a smoke screen, as in 
well-known demonstrations that 0 = 1 after sneaking in 0 as a divisor.

I don't understand why it is not just this simple.

Regards,

 - Dennis