What arithmetic corresponds to minimal logic? Starting from classical logic (Peano arithmetic, PA):


*

*Remove the law of excluded middle and we get intuitionistic logic (Heyting arithmetic, HA)

*Remove the principle of explosion and we get minimal logic (but what arithmetic?)

 A: This system lacks a standard, widely-accepted name. (How does one prove a negative? How about the question asking for a standard name was left unanswered for 3+ years on a Q/A site frequented by experts?) For now, let's call this system PAML (Peano Axioms in Minimal Logic).
Studying PAML is not fundamentally different from studying Heyting arithmetic, thanks to the following theorem: 

Let $\varphi$ be a formula of Heyting arithmetic (with negation $\neg P$ defined as $P \rightarrow \bot$). Let $\varphi^{0=1}$ denote the formula obtained by replacing each occurrence of $\bot$ in $\varphi$ with the formula $0 = 1$. Then PAML proves $\varphi^{0=1}$ precisely if Heyting arithmetic proves $\varphi$.

The proof of this statement simply translates HA-proofs into PAML-proofs, replacing every use of ex falso quodlibet $\bot \rightarrow A$ by a tailor-made proof of $0=1 \rightarrow A^{0=1}$. This is done by induction on the structure of $A$. We'll do the base case, as the inductive cases are straightforward.
If $A$ is atomic, then it either has the form $t_1 = t_2$ for terms $t_1,t_2$, or the form $\bot$. In the latter case we have to prove $0=1 \rightarrow 0=1$, which is easy. In the former case we have to prove $0=1 \rightarrow t_1 = t_2$. We can use the following argument. Assume $0=1$, multiply both sides by $t_1$ and use the usual facts about multiplication to obtain $0 = t_1$. Similarly, $0 = t_2$. Hence $t_1 = t_2$.
