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

intuitionistic-logiclogicmodel-theory

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.

Best Answer

$\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

Related Question