Constructive proofs and omega-consistency 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 ?

PA is not constructive in this sense. For note

> $PA \vdash \exists x(\varphi(x) \lor \forall y\
eg\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\
eg 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.