Why the fact that $\mathbb{N}$ has decidable equality does not imply $\mathsf{HA} = \mathsf{PA}$?

Question

It is well-known that the natural numbers has decidable equality, the property that for any $n, m \in \mathbb{N}$ $$ n=m \lor n \neq m .$$ In fact, this is not so difficult to prove by double induction. Moreover, equality is the only relation contained in the signature of intuitionistic number theory ($\mathsf{HA}$), meaning that any atomic proposition of it will have the form of $n = m$.

So why is that this does not imply the law of excluded middle, which says that $$ P \lor \neg P$$ for every proposition $P$? Clearly, we have the base case. Does this argument breaks down in the inductive step? In this case, it fails for which connectives?

Disjunction, perhaps? Well, it doesn't seem so. For suppose that $P$ has the form $ (n = m \lor i = j)$. Then our goal $$ (n = m \lor i = j) \lor \neg (n = m \lor i = j) $$ is the same as $$ (n = m \lor i = j) \lor (n \neq m \land i \neq j) $$ which by distributivity we obtain $$ (n \neq m \lor (n = m \lor i = j)) \land (i \neq j \lor (n = m \lor i = j))$$ and by associativity we have $$ ((n = m \lor n \neq m) \lor i = j) \land (n = m \lor (i = j \lor i \neq j))$$ this, however, is true, since both $n=m \lor n \neq m$ and $i=j \lor i \neq j$ are the case. So where exactly is the point the argument breaks down? Otherwise, $\mathsf{HA}=\mathsf{PA}$, which is obviously false.

Answer 1

It's the induction step where this breaks down - specifically, once we introduce quantifiers. Consider a sentence of the form $\forall x\exists y\varphi(x, y)$ where there is no computable function $f$ such that for all naturals $n$, $\varphi(n, f(n))$ holds (coming up with such a sentence is a good exercise). LEM will fail for such a sentence in HA.

Answer 2

As Noah Schweber says, the issue is with quantifiers. Here are three remarks that are too long for comments:

1. HA has the disjunction property: if HA proves $\phi \lor \psi$ then HA proves $\phi$ or HA proves $\psi$. Suppose $\tau$ is a true sentence that is not provable in HA (these must exist by the incompleteness theorem). HA cannot prove false sentences, so HA cannot prove $\lnot \tau$. By the disjunction property, this means that HA cannot prove $\tau \lor \lnot \tau$, so excluded middle fails for every true sentence unprovable in HA. This is the method I would use to solve the question Noah posed.

2. We can use bullet 1 to make examples at very low levels of the arithmetical hierarchy. HA does not prove the true sentence $\text{Con}(\text{HA})$ which is $\Pi^0_1$, so the law of the excluded middle fails for $\Pi^0_1$ sentences. Similarly, if we let $\text{InCon}(\text{HA})$ be $\Sigma^0_1$ sentence which is classically the negation of $\text{Con}(\text{HA})$, then HA cannot prove $\text{InCon}(\text{HA})$ (because that sentence is false) but HA cannot prove $\lnot \text{InCon}(\text{HA})$ either, which means that the law of the excluded middle fails for $\Sigma^0_1$ sentences as well. One way to see that $\lnot \text{InCon}(\text{HA})$ is not provable in HA is that $\text{InCon}(\text{PA})$ holds in some model of PA, and this is also a model of HA, and PA proves $\text{InCon}(\text{PA}) \to \text{InCon}(\text{HA})$ via a double-negation interpretation. So there is a model of $\text{HA} + \text{InCon}(\text{HA})$.

3. The question body focuses on disjunction, but in the context of HA (and intuitionistic arithmetic more generally), we can define disjunction in terms of the other connectives, so $\phi \lor \psi$ is defined as $$(\exists n)[(n = 0 \to \phi) \land (n \ne 0 \to \psi)].$$ Therefore, when we want to prove something about HA by induction on the complexity of a formula, and the thing we are proving doesn't mind if we replace each formula with a provably equivalent one, we can skip the case for disjunction. That latter condition holds for LEM.