# Prime Formulas in Heyting Arithmetic

I have been reading into Intuitionistic Logic, namely Heyting arithmetic, and I've bumped into this:

Corollary 3.9. Let $A_0$ be a quantifier-free formula of $\mathscr L(HA)$. Then $$HA\vdash A_0\lor\lnot A_0$$ In particular, quantifier-free formulas are provably stable, i.e. $$HA\vdash\lnot\lnot A_0\to A_0$$

Seemingly, this is a form of the LEM, but I thought this was rejected in Intuitionistic Logic? Further reading suggests that this can be shown using the fact that all prime formulas are of the form $s=t$, and thus their Godel-Gentzen translation $g(s=t)$ =$\neg\neg (s=t)$ = ($s=t$). Again, I didn't think this double negation was permitted in Intuitionistic logic?

• The law of the excluded middle is not really rejected in intuitionistic logic; instead it is just not provable (that is, not included as an axiom and not provable from the other axioms). Heyting Arithmetic is compatible with the law of the excluded middle in the sense that every classical model of Peano arithmetic is also a model of Heyting Arithmetic. So the law of the excluded middle is not disprovable in Heyting Arithmetic. – Carl Mummert Jan 26 '16 at 1:45

Double negation is certainly allowed in intuitionistic logic (IL). The grammar is the same as for classical logic: they have the same well-formed formulas. But $\neg\neg p\to p$ (equivalent to LEM) is not a theorem of IL, for arbitrary formulas $p$.
• So for $\neg\neg (s=t)=(s=t)$. Given its intuitionistic setting, this is interpreted as $((s=t) \Rightarrow \bot) \Rightarrow \bot) \Rightarrow (s=t)$. I can't see how this holds... – Dennis Jan 26 '16 at 2:00
• Here, $s, t$ are presumably closed terms, with no free variables. Each denotes a particular integer. – BrianO Jan 26 '16 at 2:05