Explosion and Cut Required
dennis.hamilton at acm.org
dennis.hamilton at acm.org
Wed Jun 15 13:20:21 EDT 2022
> -----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
More information about the FOM
mailing list