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

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.

• Just a comment: if you can really quantify over propositions, then instead of taking $\dot\neg A$ to be $A \to F$, you could take it to be $\forall F . A \to F$. In the presence of $\bot$ and explosion, $\forall F . A \to F$ is equivalent to $A \to \bot$. Jul 15 '20 at 22:38
• @ZhenLin That's true. I think I have to rewrite my question a bit to clearify that the quantificatition is to be understood differently here. I want to use it in a meta way to say for example "Assume I add every instance of LEM as an axiom, then I can show DN for every proposition". Jul 16 '20 at 6:28
• Check out this paper: arxiv.org/pdf/1304.0272.pdf, but it only considers LEM, DN, and Ex Falso. I like to see this verified in Coq, but I don't know Coq yet (TnT). Also, it is in Sequent Calculus. Jul 16 '20 at 9:41
• @Poypoyan Thanks for this reference! Its quite helpful. I can adapt my question now a little bit; by the result of the paper it comes down to less implications being possible or not. Jul 17 '20 at 7:14
• $\mathsf{Pierce}$ is the only law that does not use this fake negation. So, I wonder how one could conclude the existence of some arbitrary propositional variable ($F$) that has the $\mathsf{Explosion}$ property, from a law that has no information about $F$ or this "fake" negation. Jul 17 '20 at 10:45

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