Heyting arithmetic

Remarks

Example: HA proves $\forall x\, \forall y\, (x = y \vee \neg x = y)$, by induction on $x$ and $y$. So excluded middle holds in HA for equations, and, by induction on formulas, for all formulas without unbounded quantifiers. Non-example: HA does not prove $\forall x\, (\exists y\, T(x, x, y) \vee \neg \exists y\, T(x, x, y))$, where $T$ is Kleene's predicate for "program $x$ on input $x$ halts within $y$ steps". This formula is provable in PA, so the two theories differ. HA has the disjunction property: if HA proves a closed formula $A \vee B$, then it proves $A$ or it proves $B$. It has the existence property: if HA proves a closed formula $\exists x\, A(x)$, then it proves $A(\overline{n})$ for some numeral $\overline{n}$.