Rule of Explosion/Proof Rule

Proof Rule

The rule of explosion is a valid argument in certain types of logic dealing with contradiction $\bot$.

This includes classical propositional logic and predicate logic, and in particular natural deduction, but for example not Johansson's minimal logic.

As a proof rule it is expressed in the form:

If a contradiction can be concluded, it is possible to infer any statement $\phi$.

It can be written:

$\ds {\bot \over \phi} \bot_e$

Tableau Form

Let $\phi$ be a well-formed formula.

The Rule of Explosion is invoked in the following manner:

			Pool:					The pooled assumptions of the occurrence of $\bot$
			Formula:					$\phi$
			Description:					Rule of Explosion
			Depends on:					The line containing the occurrence of $\bot$
			Abbreviation:					$\bot \EE$

Explanation

The Rule of Explosion can be expressed in natural language as:

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 kangaroo."

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 is certainly human.

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

Also known as

The Rule of Explosion is also known as the rule of bottom-elimination.

Those who fancy Latin may like ex falso (sequitur) quodlibet, which literally means from a falsehood (follows) whatever you like.

Also see

• This is a rule of inference of the following proof systems:
  • Definition:Natural Deduction

Technical Note

When invoking the Rule of Explosion in a tableau proof, use the {{Explosion}} template:

{{Explosion|line|pool|statement|depends}}

or:

{{Explosion|line|pool|statement|depends|comment}}

where:

line is the number of the line on the tableau proof where Rule of Explosion is to be invoked

pool is the pool of assumptions (comma-separated list)

statement is the statement of logic that is to be displayed in the Formula column, without the $ ... $ delimiters

depends is the line of the tableau proof upon which this line directly depends, the one with $\bot$ on it

comment is the (optional) comment that is to be displayed in the Notes column.

Sources

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