Forcing in Second-Order Arithmetic

Question

If I understand correctly, Stephen Simpson, in his book Subsystems of Second Order Arithmetic, deems second-order arithmetic as a two-sorted first-order theory. If this is correct, then it seems reasonable to infer that one could use forcing to add generic sets of integers ('reals') and form models of $SOA$ that contain nonconstructible sets of integers--indeed, one could hypothetically form models of $SOA$ in which the sets of integers form a proper class. The purpose of such an exercise would be to study ordinary mathematics in such models for the purpose of studying what role nonconstructible sets would play in ordinary mathematics if mathematical practice advanced sufficiently to where such sets were 'needed'. I am wondering if there are any papers in the literature where such models of $SOA$ have been studied. Thanks in advance for any help given.

Answer 1

Re: the sets of natural numbers forming a proper class, they always do in second-order arithmetic: there is no sort for sets of sets of numbers! So there's no distinction between collections of sets of naturals which are sets, and collections of sets of naturals which aren't sets. All there is to a model of $RCA_0$ is: the natural numbers, and the sets of natural numbers.

Forcing does indeed work in second-order arithmetic. The idea is to expand the second-order part of a model $(N, S)\models RCA_0$; e.g., beginning with $M=(\omega, REC)$ (standard naturals, and recursive sets only), we can force to add (say) a Cohen-generic real $G$; the resulting model is $M[G]=(\omega, REC[G])$, that is, standard naturals and reals Turing below $G$.

Usually in second-order arithmetic we're more interested in iterated forcing: e.g. to build a model of $WKL_0+\neg ACA_0$, we iterate Jockusch-Soare forcing (from the Low Basis Theorem) over REC. There are exceptions, however: e.g. in Steel forcing, we perform a single forcing extension, and then look at a submodel of the result (Steel's original paper is quite readable) - similar to, but not the same as, a symmetric submodel. Basically, the full Steel extension is $M[G]$, and breaks into "layers" $M[G]_\alpha$ for $\alpha\in \omega_1^{CK}\cup\{\infty\}$; the model $M'$ we want is $\bigcup_{\alpha\in\omega_1^{CK}} M[G]_\alpha$, that is, the "ranked" part of $M[G]$.

The following description I think will be helpful to you: suppose I have a model $M=(\omega, S)$ of $RCA_0$, with standard natural numbers. This model $M$ lives in a universe $V$ of set theory. I'll force over $V$ with some poset $\mathbb{P}$ to get a generic object $G$; then, having fixed some names for reals $\nu_i$ ($i\in I$) in advance, I'll look at the structure $$M'=(\omega, \{r: \exists a_1, . . . , a_n\in S, i_1, . . . , i_m\in I(r\le_T a_1\oplus...\oplus a_n\oplus \nu_{i_1}[G]\oplus . . . \oplus\nu_{i_m}[G])\}),$$ that is, every real you can compute from things in $S$ together with things named by $\nu_i$s. This picture works less well for forcing over nonstandard models (although with some effort it can still be useful), but over standard models it clarifies things a lot. It's especially useful in contexts where the forcing you're performing isn't adequately coded by a single real: e.g. Steel forcing, Hechler forcing, etc. In these forcings, a name for a real is not, on the face of it, coded by a real, and so defining the generic extension can get a bit messy.

You mention examining the role of nonconstructible sets in mathematical practice. This seems like a job for ZFC as a base theory, instead; I don't really see how second-order arithmetic is the right context for this.