Excluded middle, double negation, contraposition and Peirce's law in minimal logic

Question

Minimal logic does not assume any falsity $\bot$ or negation $\neg$, so the above mentioned laws can (apart from Peirce's) not be stated as usual. However, if we fix some propositional variable $F$, we can use it to define a kind of negation by $\dot\neg A := A \rightarrow F$. We can then define \begin{align} \mathsf{LEM} &:= \forall A. ~\vdash_m A ~\lor~ \dot\neg A \\ \mathsf{DN} & := \forall A. ~\vdash_m \dot\neg\dot\neg A \rightarrow A \\ \mathsf{CP} & := \forall A~B. ~\vdash_m (\dot\neg B \rightarrow \dot\neg A) \rightarrow (A \rightarrow B) \\ \mathsf{Peirce} & := \forall A ~B. ~\vdash_m ((A \rightarrow B) \rightarrow A)\rightarrow A \end{align}

where $A, B$ are propositions$^{(\ast)}$ and $\vdash_m$ stands for derivability in minimal logic. In intuitionistic logic (taking $F = \bot$ and $\vdash_i$ instead) they can all be shown to be equivalent.

In minimal logic, I succeeded in proving: $$ \mathsf{DN} \leftrightarrow \mathsf{CP} ~~~,~~~ \mathsf{CP} \rightarrow \mathsf{Peirce} ~~~,~~~ \mathsf{Peirce} \rightarrow \mathsf{LEM} $$ The intuitionistic proofs I did for the other implications all needed the explosion principle and, at least to me, there seems to be no way of avoiding this. I don't know much about the semantics of minimal logic, so my question comes down to:

Can the other implications be shown or is there some semantics showing the impossibility?

I did the proofs in part on paper and checked all of them in Coq by formalizing the deduction system for propositional minimal logic. (There is also MINLOG, but I have not worked with it so far)

---

$(\ast)$ The quantification here is not supposed to be internal to the logic. I am only considering propositional minimal logic here. So for example, $\mathsf{LEM} \rightarrow \mathsf{DN}$ should be understood as "adding every instance of $A \lor \dot\neg A$ as an axiom, I can derive $\dot\neg \dot\neg B \rightarrow B$ for every proposition $B$".

---

Update (5. April 2021): Today I found this paper

Classifying Material Implications over Minimal Logic (Hannes Diener and Maarten McKubre-Jordens)

Which pretty much sums up everything I wanted to know and more.

Answer 1

$\mathsf{Peirce}$ is stronger than $\mathsf{LEM}$, but it happens to be interderivable with generalised excluded middle $(\mathsf{GEM})$ $$ \mathsf{GEM} := \forall A~B. ~\vdash_m A ~\lor~ (A \rightarrow B). $$

A weak form of Pierce's law is interderivable with $\mathsf{LEM}$ $$ \mathsf{WPierce} := \forall A. ~\vdash_m (\dot\neg A \rightarrow A) \rightarrow A. $$

None of these four principles are enough to derive $\mathsf{Explosion}$. These results, as well as ones that you mention in your question body, are listed as proposition 3 in Minimal Classical Logic and Control Operators by Zena M. Ariola and Hugo Herbelin

Answer 2

Using the results form the paper mentioned in the update, there is another way we can argue why $\mathsf{Peirce} \rightarrow \mathsf{Explosion}$ can not be possible.

Assume it holds, then it means we have a way of deducing $\forall A. \vdash_m F \rightarrow A$ from $\mathsf{Peirce}$. Since $F$ does not appear in $\mathsf{Peirce}$, this means we can use practically the same deduction to show $\forall A. \vdash_m B \rightarrow A$ for any propositional variable $B$, not only the particular choice $B = F$. So we get $$ \forall B~A. ~\vdash_m B \rightarrow A $$ This implies, that for any $X$ we have $\vdash_m (X \rightarrow X) \rightarrow X$ which in turn implies $\vdash_m X$. So we would have the highly problematic $\forall X. \vdash_m X$.