Constructive proofs and omega-consistency

Question

That old MSE question discusses the notion of “constructive proof”, and the answers explain that there is no one definition of what "constructive" or "non-constructive" means.

Recently, I thought of the following definition : let us say a theory $T$ (at least as strong as Peano arithmetic, say) is “constructive” if whenever a nonconstructive proof about integers exists, then there is a constructive equivalent, i.e. whenever $T$ proves (“non-constructively”) that $\exists \ \text{integer } n,\ \phi(n)$ for some predicate $\phi$, then there is an integer $n_0$ such that $T$ proves $\phi(n_0)$.

There is a connection between this notion and $\omega$-consistency : if $T$ is consistent but $\omega$-inconsistent, then T is not “constructive”. But (unless I missed something), if we only know $T$ is $\omega$-consistent, we cannot know in advance if $T$ will be constructive or not.

Is it known whether PA,ZF or ZFC are “constructive” in this sense ?

Answer 1

PA is not constructive in this sense. For note

$PA \vdash \exists x(\varphi(x) \lor \forall y\neg\varphi(y))$.

Now take the case where $\varphi(x)$ is $T(e,e,x)$, which expresses the relation which holds when $x$ codes the steps in a halting computation by Turing machine number $e$ run on input $e$. This Kleene relation is decidable, and indeed is expressible in the language of $PA$. If, for given $e$, there were always a number $n$ such that

$PA \vdash (T(e, e, n) \lor \forall y\neg T(e, e, y))$,

then we could do a terminating search for $n$ given $e$ by enumerating $PA$ proofs, and by then deciding whether $T(e,e,n)$ it would be decided whether Turing machine $e$ halts on input $e$, assuming $PA$ is sound. But we know the halting problem is undecidable.

Answer 2

This property is called the "numerical existence property". It is common in constructive systems and rare in systems with classical logic. There is an article on Wikipedia that lists several references.