# Is the rule of explosion (aka ex falso sequitur quodlibet) something that needs to be proved?

On this and this pages, there are proofs presented for this rule, but what confuses me though is that I think we actually need to show that $\bot\vdash Q$ holds, not $(P\wedge\neg P)\vdash Q$ or $\vdash(P\wedge\neg P)\rightarrow Q$. I know that $P\wedge\neg P$ is an obvious contradiction and in the natural deduction system I have seen you introduce a $\bot$ from $P$ and $\neg P$ on two separate lines, but still I don't think this necessarily means that $\bot$ is equivalent to $P\wedge\neg P$!

• In Natural Deduction we have two basic possibilities: (i) $\bot$ as primitive, with the rule $\bot \vdash \varphi$ and $\lnot$ defiend. In this case, the intro- and elimination-rules for $\lnot$ are derived from those for $\to$ using the abbreviation: $\lnot P := P \to \bot$. – Mauro ALLEGRANZA Sep 25 '17 at 11:44
• (ii) $\lnot$ as primitive with the "usual" intro- and elimination-rules. – Mauro ALLEGRANZA Sep 25 '17 at 11:45
• @MauroALLEGRANZA So I guess in first case you don't need to derive this rule you just take it for accepted, and in the second one you don't even use $\bot$ symbol instead you use something like $P\wedge\neg P$ and those proofs are for this second case? – Pooria Sep 25 '17 at 12:22
• Correct; in the second case, the Ex falso "axiom" will be like: $\lnot A \to (A \to B)$. – Mauro ALLEGRANZA Sep 25 '17 at 19:03