3
$\begingroup$

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?

$\endgroup$
1
  • 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
    Commented Jan 26, 2016 at 1:45

1 Answer 1

Reset to default
5
$\begingroup$

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.

$\endgroup$
3
  • $\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
    Commented Jan 26, 2016 at 2:00
  • $\begingroup$ Here, $s, t$ are presumably closed terms, with no free variables. Each denotes a particular integer. $\endgroup$
    – BrianO
    Commented Jan 26, 2016 at 2:05
  • $\begingroup$ @BrianO even if they contained free variables, I'm pretty sure HA proves the decidability of natural equality, which suffices $\endgroup$
    – univalence
    Commented Mar 11, 2021 at 14:02

You must log in to answer this question.

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