# Is Heyting arithmetic sufficient to prove its own (formalized) existence property?

Let $$\mathsf{HA}$$ denote first-order Heyting arithmetic (viꝫ., Peano axioms with unrestricted recursion scheme, in first-order intuitionistic logic). It is known (e.g., Troelstra & van Dalen, Constructivism in Mathematics (1988), 3.5.6; Beeson, Foundations of Constructive Mathematics (1985), VII.5.3 but concerning a different system; or Troelstra (ed), Metamathematical Investigations of Intuitionistic Arithmetic and Analysis (1973), 3.1.5) that $$\mathsf{HA}$$ has the number existence property:

(NEP) If $$\mathsf{HA} \vdash \exists n. P(n)$$ for some closed formula $$\exists n. P(n)$$, then in fact there is a natural number $$n$$ such that $$\mathsf{HA} \vdash P(\overline{n})$$ (with $$\overline{n}$$ the obvious term that denotes $$n$$).

Now this number existence property be formalized as a statement of arithmetic $$\forall “P”.((\mathsf{HA} \vdash \exists n. P(n)) \Rightarrow \exists n. (\mathsf{HA} \vdash P(\overline{n})))$$, beginning with a universal quantifier ranging over Gödel codes for formulas $$P$$. So we can ask whether $$\mathsf{HA}$$ proves this formalized number existence property.

The techniques used to prove NEP in the references above all seem impossible to formalize in $$\mathsf{HA}$$, because they depend on something (like cut-elimination or formalization of arithmetical truth) that is beyond its power. Yet I also don't see how NEP would imply the consistency of $$\mathsf{HA}$$. So here are my questions:

Questions:

1. Does $$\mathsf{HA}$$ prove the (formalized) number existence property, $$\forall “P”.((\mathsf{HA} \vdash \exists n. P(n)) \Rightarrow \exists n. (\mathsf{HA} \vdash P(\overline{n})))$$, for $$\mathsf{HA}$$?

2. If not, does it at least prove $$((\mathsf{HA} \vdash \exists n. P(n)) \Rightarrow \exists n. (\mathsf{HA} \vdash P(\overline{n})))$$ for each $$P$$?

3. If a negative answer to (1), does $$\forall “P”.((\mathsf{HA} \vdash \exists n. P(n)) \Rightarrow \exists n. (\mathsf{HA} \vdash P(\overline{n})))$$ imply the consistency of $$\mathsf{HA}$$?

4. If a negative answer to (2), does $$((\mathsf{HA} \vdash \exists n. P(n)) \Rightarrow \exists n. (\mathsf{HA} \vdash P(\overline{n})))$$ imply the consistency of $$\mathsf{HA}$$ for some judiciously chosen $$P$$?

On the other hand, considering the special case where $$P$$ is $$\Delta_0$$, the schema in 2 implies (classically, to make things simpler) “HA is inconsistent or $$\Sigma_1$$-sound”. More precisely, if HA proved 2, then PA + Con(PA) would prove the local $$\Sigma_1$$-reflection principle for HA, which implies the same principle for PA by (HA-verifiable) $$\Sigma_1$$-conservativity. Thus, PA + Con(PA) would prove its own consistency, contradicting Gödel’s theorem.
• The argument that schema (2) falls foul of Gödel’s theorem can be given a bit more elementarily, and constructively. Taking $P(n)$ to be the property “$n$ is a proof of false in HA”, schema (2) gives “if HA proves “HA is inconsistent”, then HA is inconsistent” (since being a proof is an arithmetical property). Contrapositively, this implies “if HA is consistent, then HA doesn’t prove ‘HA is inconsistent’”; in other words, “Con(HA) implies Con(HA + Con(HA))”. If this was provable in HA, then HA + Con(HA) would prove its own consistency, contra Gödel. Jan 12, 2022 at 12:10
• You are right. The reason I formulated it with $\Sigma_1$-soundness is that (at least classically) some form of it actually implies the numerical existence property for HA, hence one can obtain an exact characterization in this way. But this requires much more effort. Jan 12, 2022 at 12:30
• Specifically, I'm not sure how to exactly characterize the weaker schema 2, but I believe that the uniform statement of the number existence property as in question 1 is equivalent over HA to the statement $\forall\phi\in\Sigma_1\,(\Box\phi\to\Box\bot\lor\mathrm{Tr}(\phi))$, where $\Box$ denotes the formalized provability predicate for either HA or PA, and Tr is a truth predicate for $\Sigma_1$ sentences. Over PA, this is equivalent to the disjunction of inconsistency with the uniform $\Sigma_1$-reflection principle. Jan 12, 2022 at 19:51