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:
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 invokedpool
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$ ... $
delimitersdepends
is the line of the tableau proof upon which this line directly depends, the one with $\bot$ on itcomment
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