Propositional Logic: Natural deduction
Contradiction elimination rule
With the rules of reasoning that we have covered so far, there are still tautologies that we cannot derive:
- \(\neg\, p\rightarrow (p\rightarrow q)\), known by its Latin name ex falso seguitur quod libet ("anything follows from an absurdity"). So this formula states that if \(p\) is false, then any proposition \(q\) (quod libet) can be derived from the fact that \(p\) is true. In other words, if a contradiction can be derived, then any arbitrary conclusion is allowed.
- \(p\lor \neg\,p\), known as the rule of excluded third.
In this theory page we discuss which reasoning rule we need so that we can derive \(\neg\, p\rightarrow (p\rightarrow q)\). In the theory page that follows, we discuss the reasoning rule with which the tautology \(p\lor \neg\,p\) can be derived.
Elimination rule for contradiction The elimination \(\bot\,\mathrm{E}\) for the falsum \(\bot\), which represents an always false proposition is as follows: \[\begin{array}{l|ll} \vdots & \vdots &\\ k &\bot & \\ \vdots & \vdots & \\ l & \varphi& \bot\,\mathrm{E}, k \end{array}\]
With the contradiction reasoning rule, the formula \(\neg\, p\rightarrow (p\rightarrow q)\) can be derived without premises:
The contraction reasoning rule is also needed to derive the tautology \[p\lor q, \neg\, p \vdash q\] :
Unlock full access
