Are there "non-constructive" sets in second-order arithmetic?

Question

Consider $\phi(A)$ a formula of second-order arithmetic with one free variable $A$ of type "set". Suppose $\exists A : \phi(A)$ is a true sentence. Does it follow (not in second order arithmetic itself, but in a stronger theory of your choice, e.g. ZFC) that there is a formula of second-order arithmetic $\psi(n)$ with one free variable $n$ of type "number", such that $\phi(\lbrace n | \psi(n)\rbrace)$ is a true sentence?

Answer 1

This may or may not be true depending on the background set theory.

On the one hand, it is consistent with ZFC that there exists a $\Delta^1_2$-definable well-ordering $\prec$ of the reals. Then one can take for $\psi(n)$ the formula saying “$n$ is in the $\prec$-minimal set $A$ satisfying $\phi(A)$”, so the answer is positive.

On the other hand, it is also consistent with ZFC that the answer is negative. For example, assume that $V$ is the Cohen forcing extension of $L$, and take for $\phi(A)$ the $\Pi^1_2$ formula saying “$A$ is not constructible”. Then $\exists A\,\phi(A)$ is true, but since Cohen forcing is homogeneous, every parameter-free definable set (not just in the language of second-order arithmetic, but in full language of ZFC) is in the ground model, which contains no witnesses to $\phi(A)$.

On the third hand, ZFC proves the answer is positive when $\phi(A)$ is $\Sigma^1_2$: if there exists an $A$ such that $\phi(A)$, there also exists such an $A$ in $L$ by Shoenfield absoluteness, and we can define a particular one using a well-ordering of constructible reals as in the first part of the answer.

Answer 2

Edit: I have expanded my original post somewhat. It's still marked as community wiki.

The question can be read in several ways, depending on the order in which the quantifiers are ordered. The answer by Emil Jeřábek addresses the following interpretation:

Does ZFC prove the following: "For every formula $\phi(A)$ of second order arithmetic there is a formula $\psi(n)$ of second order arithmetic such that $(\exists A)\phi(A) $ implies $\phi(\{n : \psi(n)\})$".

That is one reasonable interpretation of the question. But it is not the interpretation I had in mind when I read the question, because the formula $\phi$ is chosen before any mention of ZFC.

This is an particularly common issue in proof theory: there is an important difference between "if $\phi(A)$ is a true formula of second-order arithmetic, then ZFC proves ..." and "ZFC proves that if $\phi(A)$ is true a formula of second-order arithmetic, then ...".

When I read the question, it struck me as asking about something like the witness property that is commonly considered in constructive mathematics. The witness property theory for a theory with a particular language of formulas $L$ and a particular language of terms $T$ says that if the theory proves $(\exists X) \phi(X)$ for some $\phi(X) \in L$ then the theory proves $\phi(t)$ for some term $t \in T$.

For example, higher-order Heyting arithmetic has the term existence property for formulas with one free natural number variable and terms of the form $S(S(S(\cdots S(0)\cdots)))$ from the language of arithmetic.

I will explain my reading of the question, and then I will explain why it has a negative answer (with no additional set theoretic hypotheses in the metatheory). If this was not the question that was intended, it is still an interesting (although somewhat trivial) result, in my opinion. It fits with the general intuition that classical theories are not likely to have strong witness properties.

An alternative reading of the question

My first thought about the meaning of the quote from the question is that we want to prove:

If $(\exists X)\phi(X)$ is true then there is a formula $\psi(n)$ of second-order arithmetic such that $\text{ZFC}\vdash \phi(\{n : \psi(n)\})$

A moment's reflection shows that this can only work if ZFC proves $(\exists X)\phi(X)$ in the first place. So it appears that we want to prove:

If $\phi(X)$ is a formula of second-order arithmetic such that $\text{ZFC} \vdash (\exists X)\phi(X)$ then there is a formula $\psi(n)$ of second-order arithmetic such that $\text{ZFC}\vdash \phi(\{n : \psi(n)\})$

Now we are getting into the territory of a witness property for ZFC. The language of formulas consists of all second-order formulas with one free set variable; the term language consists of terms of the form $\{n : \psi(n)\}$ where $\psi(n)$ is a formula of second order arithmetic.

There is one more subtlety. What about: $$ \phi(X) \equiv (\{0\} = X \land V = L ) \lor (\{1\} = X \land \lnot (V = L) ) $$ Note that $V = L$ here is an abbreviation for ``every real is constructible" which can be expressed as a formula of second-order arithmetic. In this case, we can find $\psi$; one possibility is: $$ \psi(n) \equiv (0 = n \land V = L ) \lor (1 = n \land \lnot (V = L )) $$ So we cannot hope for the interpretation of $\psi$ to be absolute, nor can we hope for some sort of extensionality with $\{n : \psi(n)\}$, as the wording of the question might suggest. The set defined by $\psi$ may (necessarily) change from one model to another even though $\psi$ itself stays the same. Thus our proof in ZFC has to see $\psi$ itself, not just a code for $\{ n : \psi(n)\}$.

But we will show that the overall question has a negative answer anyway.

Negative answer

Using a construction similar to the answer by Emil Jeřábek, let $\phi(A)$ say: "If there is a nonconstructible real then $A$ is a nonconstructible real". Clearly $\text{ZFC}\vdash (\exists A)\phi(A)$. But there can be no $\psi$ such that $\text{ZFC} \vdash \phi(\{n :\psi(n)\})$, for the same reason as the negative answer in that other answer. If we look at the particular model of ZFC in which $V$ is a Cohen forcing extension of $L$, then no $\psi$ can define a nonconstructible real in that model.

There is some restriction in the counterexample $\phi$ we could use here. Because of Shoenfield's absoluteness theorem, ZFC does have witness property in question for formulas that are sufficiently low in the analytical hierarchy. For such formulas, ZFC proves that if $(\exists A)\phi(A)$ then $(\exists X \in L)\phi(A)$ and then $\psi$ can be a formula which defines the least set, under the $\Delta^1_2$ well ordering of $L$, which satisfies $\phi$.