Circularity of LEM, principle of explosion, and $\lnot \lnot$ elimination

Question

Consider the following proof of the principle of explosion using $\lnot \lnot$ elim:

|Assume $p \land \lnot p$

$\quad$|$p$ (from $\land$ elim)

$\quad$|$\lnot p$ (from $\land$ elim)

$\quad$|Assume $\lnot q$

$\quad$$\quad$|$p$ (restatement)

$\quad$|$\lnot q \to p$ (from $\to$ intro)

$\quad$|Assume $\lnot q$

$\quad$$\quad$|$\lnot p$ (restatement)

$\quad$|$\lnot q \to \lnot p$ (from $\to$ intro)

$\quad$|$\lnot \lnot q$ (from $\lnot$ intro)

$\quad$|$q$ (from $\lnot \lnot$ elim)

|$p \land \lnot p \to q$ (from $\to$ intro)

Consider also the proof of LEM using $\lnot \lnot$ elim:

|Assume $\lnot(p \lor \lnot p)$

$\quad$|$\lnot(p \lor \lnot p)$ (restatement)

|$\lnot(p \lor \lnot p) \to \lnot(p \lor \lnot p)$ (from $\to$ intro)

|Assume $\lnot(p \lor \lnot p)$

$\quad$|Assume $p$

$\quad$$\quad$|$\lnot(p \lor \lnot p)$ (restatement)

$\quad$|$p \to \lnot(p \lor \lnot p)$ (from $\to$ intro)

$\quad$|Assume $p$

$\quad$$\quad$|$p \lor \lnot p$ (from $\lor$ intro)

$\quad$|$p \to p \lor \lnot p$ (from $\to$ intro)

$\quad$|$\lnot p$ (from $\lnot$ intro)

$\quad$|$p \lor \lnot p$ (from $\lor$ intro)

|$\lnot(p \lor \lnot p) \to p \lor \lnot p$ (from $\to$ intro)

|$\lnot \lnot (p \lor \lnot p)$ (from $\lnot$ intro)

|$p \lor \lnot p$ (from $\lnot \lnot$ elim)

And a proof of $\lnot \lnot$ elim if we have LEM and the principle of explosion at our disposal:

|$p \lor \lnot p$ (from LEM)

|Assume $\lnot \lnot p$

$\quad$|Assume $p$

$\quad$$\quad$| $p$ (restatement)

$\quad$|Assume $\lnot p$

$\quad$$\quad$|$\lnot p$ (restatement)

$\quad$$\quad$|$\lnot \lnot p \land \lnot p$ (from $\land$ intro)

$\quad$$\quad$|$\bot$ ($\lnot$ elim)

$\quad$$\quad$|$p$ (from $\bot$ elim / the principle of explosion)

$\quad$|$p$ (from $\lor$ elim on LEM and the two previous assumption cases)

|$\lnot \lnot p \to p$ (from $\to$ intro)

My question

Am I reading this right? These rules appear circular and interdependent. If we are granted LEM and the principle of explosion, we can derive $\lnot \lnot$ elimination, but if we're granted $\lnot \lnot$ elimination, we can derive both LEM and the principle of explosion.

Is this correct or is there a way to derive these rules from some other common means?

Answer 1

You can have a logical system with double-negation elimination and without explosion.

And you can have logical system where excluded middle and double-negation elimination are provably equivalent without the use of explosion.

The classical version of Neil Tennant's Core Logic (a sort of relevant logic) is a case in point.

Which just goes to show that the rules are not interdependent in quite the way you claim. What's happening is that you are smuggling in other albeit standard assumptions (e.g. about the correct formulation of the or-elimination rule).

Of course, in a standard classical framework, things fit together rather as you say (indeed explosion can be a derived rule).