# 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.

## 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.