Reductio ad Absurdum Propositional natural deduction

A NOTA NOTE ⊥ X, A   ⊢   ⊥ NOTI X   ⊢   NOTA

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.

X, B   ⊢   A Y, B   ⊢   NOTA RAA X, Y   ⊢   NOTB

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:

SP {A, NOTA ⊢ NOT(p IMP p)} PL {X} {i} {A} {whatever} PL {Y} {j} {NOTA} {whatever} PL {X,Y} {n} {NOT(p IMP p)} {i, j [ ] RAA} EP

For NOTI, we suppose X, A ⊢ NOT(p IMP p) and proceed as follows:

SP {X ⊢ NOTA} PL {1} {1} {p} {A} PL { } {2} {p IMP p} {1 [1] IMPI} PL {3} {3} {A} {A} PL {X,3} {k} {NOT(p IMP p)} {whatever} PL {X} {n} {NOTA} {2, k [3] RAA} EP

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.