Separating the choice scheme from the parameter-free choice scheme in second-order arithmetic

This post is motivated by a really great paper of Wojciech Guzicki from the 1970s entitled "On weaker forms of choice in second-order arithmetic" [1] that I recently stumbled on while trying to trace the history of choice principles in second-order set theory (for the choice schemes over Kelley-Morse project). Guzicki asks whether the choice scheme is equivalent to the parameter-free choice scheme (keep reading for definitions) over the second-order arithmetic theory ${\rm Z}_2$. He goes on to prove that it is possible for the parameter-free choice scheme to hold, while the choice scheme fails for a $\Pi^1_2$-assertion. First, a brief background.

Second-order arithmetic studies structures with two types of objects: numbers and sets of numbers (which we can think of as the reals). It is formalized in a two-sorted logic, which has variables and quantifiers for the primary objects, and then separate variables and quantifiers for objects that are supposed to represent collections of primary objects. By convention, lowercase letters are used for primary objects and uppercase letters for their collections. A model $\mathcal M=\langle M,+,\dot,<,0,1,\mathcal S\rangle$ of second-order arithmetic is a model of first-order arithmetic $\langle M,+,\dot,<,0,1\rangle$ together with a collection $\mathcal S$ of subsets of $M$. Axiomatizations of second-order arithmetic generally consist of ${\rm PA}$ (Peano Arithmetic) for the first-order part together with axioms specifying which sets of numbers must exist (as well as whether induction holds for formulas with second-order quantifiers). So for instance, the theory ${\rm WKL_0}$ states that any collection of numbers recursive in a set in $\mathcal S$ is also in $\mathcal S$, and whenever a set in $\mathcal S$ codes an infinite binary tree, there is another set in $\mathcal S$ coding a path through this tree. Another example is the theory ${\rm ACA_0}$, which states that any collection that is first-order definable from parameters in $\mathcal S$ is itself in $\mathcal S$. I am mainly interested in one of the strongest theories of second-order arithmetic: ${\rm Z}_2$ (because it is the arithmetic analogue of ${\rm KM}$). The theory ${\rm Z}_2$ has full comprehension and full induction, meaning that any collection (second-order) definable from parameters in $\mathcal S$ is itself in $\mathcal S$, and induction applies to all second-order formulas. If $V$ is a universe of ${\rm ZF}$ (but not necessarily choice), then its $P(\omega)$ gives a model of ${\rm Z}_2$.

The choice scheme in second-order arithmetic is a choice principle which asserts for every second-order formula $\varphi(n,X,Y)$ that whenever $\forall n\,\exists X\,\varphi(n,X,A)$ holds, then there exists a collecting set $Z$ of witnesses such that $\forall n\varphi(n,Z_n,A)$ holds (where $Z_n$ is the set appearing on the $n^{\text{th}}$-slice of $Z$). More technically $$\forall n\,\exists X\,\varphi(n,X,A)\rightarrow\exists Z\,\forall n\,\varphi(n,Z_n,A).$$ The theory ${\rm Z}_2$ proves the choice scheme for $\Sigma^1_2$-assertions, but an instance of the $\Pi^1_2$ choice scheme fails in the model of ${\rm Z}_2$ given by $P(\omega)$ of the Feferman-Lévy model of ${\rm ZF}$ [2]. The parameter-free choice scheme simply disallows parameters in $\varphi$.

Now back to Guzicki's paper. Because the paper was written at the time when forcing techniques were not yet fully developed, the forcing construction used to separate the parameter-free choice scheme from the choice scheme is not easy to understand. So instead of delving into the details, I made a guess that the argument should work by considering a symmetric submodel of the forcing extension by the product of the collapses of the first $\omega_1$-many cardinals (over $L$). The argument I give below seems to be significantly simpler than the argument of the paper, which makes me very suspicious of whether it is actually correct. So I decided to write this post and hopefully get some feedback.

Theorem: There is a model of ${\rm Z}_2$ in which the parameter-free choice scheme holds but the choice scheme fails for a $\Pi^1_2$-assertion.

Proof: We work in $L$ and force with the countable support product $$\mathbb P=\Pi_{\alpha<\omega_1}{\rm Coll}(\omega,\omega_\alpha)$$ to collapse the first $\omega_1$-many cardinals of $L$ to $\omega$. Let's say that an automorphism $\pi$ of $\mathbb P$ respects coordinates if there are automorphisms $\pi_\alpha$ of ${\rm Coll}(\omega,\omega_\alpha)$ for $\alpha<\omega_1$ such that whenever $\langle p_\alpha\mid\alpha<\omega_1\rangle\in\mathbb P$, then $\pi(p)=\langle \pi_\alpha(p_\alpha)\mid\alpha<\omega_1\rangle$. Let $\mathcal G$ be the group of all coordinate respecting automorphisms of $\mathbb P$. Let $\mathcal F$ be the filter on $\mathcal G$ generated by the sets $E_\alpha$, where $E_\alpha$ is the collection of all coordinate respecting automorphisms $\pi$ such that $\pi_\beta$ is identity for all $\beta<\alpha$. Note that $\mathcal F$ is normal: if a subgroup $\mathcal H\in \mathcal F$ and $\pi\in \mathcal G$, then $\pi H\pi^{-1}$ is in $\mathcal F$ as well. Define the symmetry group of a $\mathbb P$-name $\sigma$, ${\rm sym}^{\mathcal G}(\sigma)$ to be the collection of all $\pi\in \mathcal G$ such that $\pi(\sigma)=\sigma$. If ${\rm sym}^{\mathcal G}(\sigma)$ is in $\mathcal F$, meaning that some $E_\alpha\subseteq {\rm sym}^{\mathcal G}(\sigma)$, then $\sigma$ is symmetric. Let ${\rm HS^{\mathcal F}}$ be the collection of all hereditarily symmetric names. Let $G\subseteq \mathbb P$ be $L$-generic, and let $G_\beta$ be the restriction of $G$ to the initial segment $\Pi_{\alpha<\beta}{\rm Coll}(\omega,\omega_\alpha)$ of $\mathbb P$. Define $$N=\{\sigma_G\mid\sigma\in {\rm HS}^{\mathcal F} \}.$$

It is easy to see that the choice scheme fails in $\mathcal M$. Let $r\in\mathcal S$ be a relation on $\omega$ coding $\omega_1^L$, and let $\alpha_n$ be the ordinal coded by $n$ in $r$. The model $\mathcal M$ satisfies that for every $n\in\omega$, the code of $L_{\omega_{\alpha_n}}$ exists, but there is no collecting set of the codes of all $L_{\omega_{\alpha_n}}$ because such a set must be uncountable in $N$.

Now we argue that the choice scheme must hold for any parameter-free assertion in $\mathcal M$. Suppose that $\mathcal M\models\forall n\,\exists X\,\varphi(n,X)$. We can assume, by working below some condition if necessary, that this statement is forced by $1_{\mathbb P}$ about the canonical $\mathbb P$-name $\dot {\mathcal M}$ for $\mathcal M$. We will argue in a moment that for every $n\in\omega$, there is $\xi_n<\omega_1$ such that it is forced by $1_{\mathbb P}$ that there is $A\in L[G_{\xi_n}]$ such that $\dot{\mathcal M}\models\varphi(n,A)$. Let's finish the argument, supposing this to be the case. Since $\omega_1$ is regular in $L$, there is an upper bound $\xi<\omega_1$ for the $\xi_n$, and so $1_{\mathbb P}$ forces that all witnessing $A$ are in $L[G_\xi]$. But $P(\omega)^{L[G_\xi]}$ is countable in $N$, so that the collection of the witnessing $A$ is coded by a subset of $\omega$ in $N$ and is therefore in $\mathcal S$. It remains to prove our assumption.

Fix $n$. Since there is some $A\in\mathcal S$ such that $\mathcal M\models\varphi(n,A)$ and $A$ must be in $L[G_\xi]$ for some $\xi$, it follows that there is a condition $p\in\mathbb P$ and some ordinal $\xi<\omega_1$ such that $p$ forces that there is $A\in L[G_\xi]$ such that $\dot{\mathcal M}\models\varphi(n,A)$. If this statement is not forced by $1_{\mathbb P}$, then there is some condition $q$ forcing that this is not the case. Let $\pi$ be a coordinate respecting automorphism such that $\pi(p)$ and $q$ are compatible. But it is not difficult to see that $\pi(\dot {\mathcal M})$ and $\dot{\mathcal M}$ will be interpreted identically by any $L$-generic filter $G$ because $L[G_\alpha]=L[\pi(\dot G_\alpha)_G]$ for all $\alpha<\omega_1$ because $\pi(\dot G_\xi)_G$ is $H_\xi$ for $H=(\pi^{-1})'' G$. Thus, $\pi(p)$ forces that there is $A\in L[G_\xi]$ such that $\dot{\mathcal M}\models\varphi(n,A)$, which contradicts our assumption that $q$ forced the negation of this statement. $\square$

Incidentally, the dependent choice scheme and the parameter-free dependent choice scheme are equivalent [bibcite key=guzicki:choiceScheme]. The dependent choice scheme asserts for every second-order formula $\varphi(X,Y,W)$ that whenever $\forall X\,\exists Y\,\varphi(X,Y,A)$ holds, then we can make $\omega$-many dependent choices for the relation given by $\varphi$, meaning that there is a set $Z$ such that $\forall n\,\varphi(Z_n,Z_{n+1},A)$.

References

1. W. Guzicki, “On weaker forms of choice in second order arithmetic,” Fund. Math., vol. 93, no. 2, pp. 131–144, 1976.
2. S. G. Simpson, Subsystems of second order arithmetic, Second. Cambridge University Press, Cambridge; Association for Symbolic Logic, Poughkeepsie, NY, 2009, p. xvi+444.