14
$\begingroup$

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.

$\endgroup$
6
  • 2
    $\begingroup$ 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$. $\endgroup$
    – Zhen Lin
    Commented Jul 15, 2020 at 22:38
  • 1
    $\begingroup$ @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". $\endgroup$
    – Léreau
    Commented Jul 16, 2020 at 6:28
  • 2
    $\begingroup$ 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. $\endgroup$
    – Poypoyan
    Commented Jul 16, 2020 at 9:41
  • $\begingroup$ @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. $\endgroup$
    – Léreau
    Commented Jul 17, 2020 at 7:14
  • $\begingroup$ $\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. $\endgroup$
    – frabala
    Commented Jul 17, 2020 at 10:45

2 Answers 2

2
+50
$\begingroup$

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

$\endgroup$
1
  • $\begingroup$ Ah, thanks a lot for the reference! $\endgroup$
    – Léreau
    Commented Jul 25, 2020 at 9:53
1
$\begingroup$

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

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .