# trouble with proof for principle of explosion using primitive rules

A common proof for the principle of explosion (also known as ex falso quodlibet)

$$p, \neg p \vdash q$$

utilizes disjuncive syllogism, but I am trying to prove the principle of explosion using only the primitive rules of propositional logic. I have seen some proofs online as follows:

$$\{ 1 \} \:\:\:\:$$ $$1. p \:\:\:\:\:\:\:\:\:\:\:\:\:\:$$ premise

$$\{ 2 \} \:\:\:\:$$ $$2. \neg p \:\:\:\:\:\:\:\:\:\:\:$$ premise

$$\{ 3 \} \:\:\:\:$$ $$3. \neg q \:\:\:\:\:\:\:\:\:\:\:$$ assumption for RAA

$$\{ 1,2 \}$$ $$4. p \wedge \neg p \:\:\:\:$$ $$1,2$$ &I

$$\{ 1,2 \}$$ $$5. \neg \neg q \:\:\:\:\:\:\:\:$$ $$3,4$$ RAA

$$\{ 1,2 \}$$ $$6. q \:\:\:\:\:\:\:\:\:\:\:\:\:\:$$ $$5$$ DNE

However, I have the understanding that RAA (proof by contradiction) requires the contradiction (on line $$4$$) to depend on the assumption (on line $$3$$) in order to infer the negation of the assumption (on line $$5$$). But the dependency numbers associated with line $$4$$ do not include the assumption on line $$3$$, so I have trouble understanding why this proof is correct. Can someone clear this up for me? Thanks!

• Maybe you have to specify which is your proof system. See Natural Deduction. Commented Jul 5, 2023 at 7:38
• RAA can be negation introduction as well as proof by contradiction. There are different equivalent ways to formalize Classical Logic: RAA, DN, LEM. Commented Jul 5, 2023 at 7:38
• Having said that, the formal derivation above is correct. Commented Jul 5, 2023 at 7:42
• As Mauro says, it depends on the specific rules you want/need to use. But if the RAA rule you want to use requires that the statement to be negated is part of the assumption base, then you can always include that by a simple little trick: use &I on 3 and 4 and then &E immediately after to get back to $p\land \neg p$, but now it has 3 as part of the assumption base Commented Jul 5, 2023 at 15:57
• Thank you, @Bram28! yes, i think that technique is known as augmentation Commented Jul 5, 2023 at 22:39

Although it is appropriate to talk over a specified system, there are some threads of ideas running through the variety of systems.

With this reservation remarked, it can be said that there are two assumption discharge rules:

Conditional introduction: Assume $$\phi$$, derive $$\psi$$ and $$\phi\rightarrow\psi$$.

Negation introduction: Having derived $$\psi$$ and $$\neg\psi$$ (in the question expressed as $$p\wedge\neg p$$ ), assume $$\phi$$ and derive $$\neg\phi$$.

The conjunction $$p\wedge\neg p$$ is to state that a contradiction has occurred. However, not every system requires this step.

A comment made by Mauro ALLEGRANZA reminded me that the proof depicted in the OP is justified via augmentation, which is explained in Paul Tomassi's text Logic on pages $$63$$-$$64$$.

$$\{ 1 \} \:\:\:\:\:\:\:\:$$ $$1. p \:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:$$ premise

$$\{ 2 \} \:\:\:\:\:\:\:\:$$ $$2. \neg p \:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:$$ premise

$$\{ 3 \} \:\:\:\:\:\:\:\:$$ $$3. \neg q \:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:$$ Assumption for RAA

$$\{ 1,2 \} \:\:\:\:$$ $$4. p \wedge \neg p \:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:$$ $$1,2$$ &I

$$\{ 1,2,3 \}$$ $$5. \neg q \wedge (p \wedge \neg p) \:\:\:$$ $$3,4$$ &I

$$\{ 1,2,3 \}$$ $$6. p \wedge \neg p \:\:\:\:\:\:\:\:\:\:\:\:\:\:\:$$ $$5$$ &E

$$\{ 1,2 \} \:\:\:\:$$ $$7. \neg \neg q \:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:$$ $$3,6$$ RAA

$$\{ 1,2 \} \:\:\:\:$$ $$8. q \:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:\:$$ $$7$$ DNE

In short, even though the assumption $$\neg q$$ on line $$3$$ has nothing to do with the contradiction already present among the premises, I can force the dependency numbers of the contradiction $$p \wedge \neg p$$ on line $$6$$ to include the line number of the assumption by conjoining the two formulas via &I and then separating the conjuncts via &E. In this way, the contradiction "depends" on the assumption and I am jusitified in carrying out a proof by contradiction.

Alternatively, I did come up with another proof for the principle of explosion that uses only primitive rules but not augmentation:

$$\{ 1 \} \:\:\:\:\:\:\:\:$$ $$1. p \:\:\:\:\:\:\:\:\:\:\:\:\:\:$$ premise

$$\{ 2 \} \:\:\:\:\:\:\:\:$$ $$2. \neg p \:\:\:\:\:\:\:\:\:\:\:$$ premise

$$\{ 1 \} \:\:\:\:\:\:\:\:$$ $$3. p \vee q \:\:\:\:\:\:\:$$ $$1$$ $$\vee$$I

$$\{ 4 \} \:\:\:\:\:\:\:\:$$ $$4. \neg q \:\:\:\:\:\:\:\:\:\:\:$$ Assumption for RAA

$$\{ 5 \} \:\:\:\:\:\:\:\:$$ $$5. p \:\:\:\:\:\:\:\:\:\:\:\:\:$$ Assumption

$$\{ 2,5 \} \:\:\:\:$$ $$6. \bot \:\:\:\:\:\:\:\:\:\:\:\:$$ $$2,5$$ &I

$$\{ 7 \} \:\:\:\:\:\:\:\:$$ $$7. q \:\:\:\:\:\:\:\:\:\:\:\:\:$$ Assumption

$$\{ 4,7 \} \:\:\:\:$$ $$8. \bot \:\:\:\:\:\:\:\:\:\:\:\:$$ $$4,7$$ &I

$$\{ 1,2,4 \}$$ $$9. \bot \:\:\:\:\:\:\:\:\:\:\:\:$$ $$3,5,6,7,8$$ $$\vee$$E

$$\{ 1,2 \} \:\:$$ $$10. \neg\neg q \:\:\:\:\:\:\:\:$$ $$4,9$$ RAA

$$\{ 1,2 \} \:\:$$ $$11. q \:\:\:\:\:\:\:\:\:\:\:\:\:$$ $$10$$ DNE

Thank you to Mackey Johnstone who provided some inspiration here.

• "fails to depend on the assumption"... You can use every assumption you want. See the "typical" derivation of $P \to (Q \to P)$: you assume P and then Q and then reiterate P and then discharge Q. Commented Jul 5, 2023 at 9:27
• you just jogged my memory that I can force the dependency numbers of a derived contradiction to include the number of the assumption (even if the assumption has nothing to do with the contradiction) via augmentation. thanks! Commented Jul 5, 2023 at 9:37