Explosion and Cut Required

[Joseph Vidal-Rosset]

Le 15/06/2022 à 19:20, dennis.hamilton at acm.org a écrit :
>> -----Original Message-----
>> ]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.

If you talk about this substitution in my paper online  (
https://www.vidal-rosset.net/paraconsistent_tennants_logic_is_inconsistent.html
), where A is interpreted by this sequent

X, A |- B

and B by this one:

X, (A -> B) -> B |- B

then I repeat that it is provable in minimal logic that these sequents
are interderivable. I have called this rule DNS for "Double Deduction à
la Slaney" (that is in fact the reducibility of triple negation to one
negation, B being most often the absurdity constant):

              X, A |- B
====================== DNS
X, (A -> B) -> B  |- B

because it was implemented by Jonh Slaney for his prover for minimal
logic. Derivable in minimal logic, it is not surprising at all that it
is also derivable in Tennant's Core logic.

Now, the logical consequence of the deductibility of this DNS rule is
this rule for antisequents (¬A and ¬B):

              X, A |/- B
====================== DNS
X, (A -> B) -> B  |/- B

Because if this deduction of rule for antisequents would be false, then
either

              X, A |/- B
====================== DNS
X, (A -> B) -> B  |- B

or

              X, A |- B
====================== DNS
X, (A -> B) -> B  |/- B

could be satisfiable, in contradiction with the proof of the
interderivability of sequents A and B (done via an admissible Cut).

I do not see the least unsoundness in this substitution: because it is
provable that sequent A and sequent B are interderivable (equivalent),
then it is provable that the respective antisequents are interderivable
too.

> The same injuries arise from proffered deductions such as
>
> A, ~A |- anything (including A & ~A)
>
> when the law of excluded middle is axiomatic.

Because it is indeed provable that the intuitionistic absurdity rule  is
derivable in classical logic, I do not understand your analogy.

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

I am sorry to tell you that analogies, suggestions and feelings cannot
be considered as rebuttals.

Regards,

Jo.