Reductio ad Absurdum Propositional natural deduction
This is a technical aside to the Logic Notes, containing a proof of a fact asserted in the body of the notes. It may be skipped by anyone willing to take that assertion on trust, as it assumes rather more mathematical background than is required to follow the general exposition of logic.
The result is that the rule RAA (Reductio ad absurdum) is
equivalent in the context of the rest of the natural deduction
system to the two rules NOTI and
NOTE. notRules and raaRule, reproduced
from Chapter 3, show the rules in
question. We wish to show that any sequent not containing the
absurd constant ⊥ which is provable using
NOTI and NOTE is provable using RAA
instead, and vice versa.
In one direction, this is trivial. Any instance of RAA can be expanded by inserting ⊥ before its conclusion and then becomes an instance of NOTE followed by NOTI:
|X, B ⊢ A||Y, B ⊢ NOTA||NOTE|
|X, Y, B ⊢ ⊥||NOTI|
|X, Y ⊢ NOTB|
The input and output sequents are unaffected by this transformation, so whatever was proved using RAA is now proved without it.
The less trivial observation is that the converse is also the case: any application of NOTE or NOTI can be emulated using RAA, without resort to the special formula ⊥. The technique is to choose an absurd formula such as NOT(p IMP p) and use that in place of ⊥. We then only need to show that the inference from A and NOTA to NOT(p IMP p)a can be made using RAA, and that if any sequent X, A ⊢ NOT(p IMP p) is provable then so is X ⊢ NOTA.
The emulation of NOTE is immediate, as it amounts just to RAA with vacuous discharge:
For NOTI, we suppose X, A ⊢ NOT(p IMP p) and proceed as follows:
The upshot is that there is a formula (namely NOT(p IMP p)) which we can spell "⊥" if we wish, which can play the role of the absurd constant, allowing negation to be introduced and eliminated by RAA in place of the two official negation rules NOTI and NOTE. RAA is therefore fully equivalent in context to those two rules together.