9
$\begingroup$

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$?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
11
$\begingroup$

The answers to all the questions are negative.

First, none of the statements implies the consistency of HA, since if HA is inconsistent, all the statements trivially hold.

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.

Improve this answer
$\endgroup$
3
  • 4
    $\begingroup$ 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. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Jan 12, 2022 at 12:10
  • 1
    $\begingroup$ 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. $\endgroup$
    – Emil Jeřábek
    Commented Jan 12, 2022 at 12:30
  • 3
    $\begingroup$ 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. $\endgroup$
    – Emil Jeřábek
    Commented Jan 12, 2022 at 19:51

You must log in to answer this question.

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