Magic rule

magic rule These rules do not allow us to prove the formula $P \vee \neg P$ nor $\neg \neg P \Rightarrow P$ nor any equivalent formula. If we add one of these formulas as an axiom scheme then we can prove the others. We can also prove them by adopting the proof by contradiction proof by contradiction rule

$H \vdash P\ \mbox{by}\ contradiction$

$H, \neg P \vdash \perp$

My preference is to base arguments for these formulas on the axiom scheme $P \vee \neg P$ called the law of excluded middle because these arguments have a special status in relating logic to computation and because this law is so important in philosophical and foundational discussions. In the organization I adopt, this is the only rule which does not fit the sequent pattern and it is the only rule not constructively justifiable as we will see later. I sometimes call the rule ``magic'' based on the discussion of justification to follow.