Axiom:Rule of Bottom-Elimination

Context

The rule of bottom-elimination is one of the axioms of natural deduction.

The rule

If we can conclude a contradiction, we may infer any statement:

$\bot \vdash p$

It can be written:

$\displaystyle{\bot \over p} \bot_e$

• Abbreviation: $\bot \mathcal E$
• Deduced from: The pooled assumptions of $\bot$.
• Depends on: The line containing $\bot$.

Explanation

What this says is: if you can prove a contradiction, you can prove anything. Compare this with the colloquial expression:

"If England win the World Cup this year, then I'm a Dutchman."

The assumption is that the concept of England winning the world cup is an inherent contradiction (it being taken worldwide as a self-evident truth that England will never win the World Cup again). Therefore, if England does win the World Cup this year, then this would imply a falsehood as the author of this page does not hail from Nederland.

This rule is denied validity in the system of Johansson's minimal calculus.

Sources

• Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems (2000): $\S 1.2.1$