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?

  • 1
    $\begingroup$ 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. $\endgroup$ – 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$.

The result you cite shows that for some sentences, double negation elimination does hold in IL — namely, for atomic sentences and Boolean combinations of them. Intuitively, pun intended, an atomic sentence represents a concrete fact, which we can prove or refute. A statement involving quantifiers, however, represents in IL an assertion that we can perform a certain construction, and LEM is not true of those.

| cite | improve this answer | |
  • $\begingroup$ 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... $\endgroup$ – Dennis Jan 26 '16 at 2:00
  • $\begingroup$ Here, $s, t$ are presumably closed terms, with no free variables. Each denotes a particular integer. $\endgroup$ – BrianO Jan 26 '16 at 2:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.