trouble with proof for principle of explosion using primitive rules

Question

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!

Answer 1

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.

Answer 2

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.