# Small Implications of the Axiom of Replacement

The axiom of replacement implies the existence of sets larger than usual in mathematical practice, but can be used to prove theorems about sets of real numbers, such as Borel determinacy. This is interesting because it suggests there's some sort of recursive procedure that makes sense for sets of reals, but is not provable in ZC alone. This procedure seems like it would be of independent interest from the question of the existence of sets beyond $V_{\omega + \omega}$ in the cumulative heirarchy.

Is there a weaker axiom or recursive set of axioms that can be added to ZC that imply exactly the implications of replacement that hold for sets in $V_{\omega + \omega}$, one that explains the kind of additional constructions that replacement permits you to make?

-
So you want something like ZC+PD sort of thing? – Asaf Karagila Jan 13 '13 at 15:18
Do you mean ZC + Borel determinacy? Would that be sufficient? – arsmath Jan 13 '13 at 16:23
I don't think determinacy has much to do with the issue here. This might be of interest: mathoverflow.net/questions/12584/…. I think what's true is that collection + separation imply replacement (when some other axioms are used). – Carlo Von Schnitzel Jan 13 '13 at 19:59
For consequences on the first order theory of $(V_{\omega+1},V_\omega,\in)$ (essentially, analysis), adding $\mathsf{PD}$ to second order arithmetic should indeed suffice. (There must be a precise version of this claim in print.) – Andrés Caicedo Jan 18 '13 at 20:01

The set $M$ of all formulas $\varphi$ that are of the form $V_{\omega+\omega} \vDash \psi$ is certainly recursive. Now the set $N:=\{ \varphi\in M: ZFC \vdash \varphi\}$ is c.e.
A standard trick gives an equivalent set $N'$ which is recursive (decidable): replace the $n$-th formula in $N$ (in any computable enumeration) by an equivalent formula that is much longer that all previous ones.
Is this set $N'$ what you are looking for? I realize that it does not have the nice form you probably wanted.
I edited to clarify that I'm looking for something explicit. I get into conversations about replacement where I say "obviously, this large set exists", and someone else says "but I don't need that set," and I say "but Borel determinacy," and they say "what's that?" Which made me wonder what does replacement actually commit you to, at the level of small sets? What exactly is the extra freedom that permits you to prove things like Borel determinacy? That's something you could have an opinion on, separate of your view of large sets. (Here large = outside of $V_{\omega + \omega)$.) – arsmath Jan 13 '13 at 17:31
One can axiomatize $N$ explicitly by the sequence of formulas $\forall f\in\mathrm{Form}\,(\mathrm{Prov}_{\mathrm{ZFC}\restriction n}(\ulcorner V_{\omega+\omega}\models\dot f\urcorner)\to V_{\omega+\omega}\models f)$ for $n\in\mathbb N$, where $\mathrm{Form}$ is the set of sentences in the language of set theory, $\mathrm{Prov}$ is the provability predicate, and $\mathrm{ZFC}\restriction n$ is the list of all axioms of ZFC with Gödel number $\le n$. – Emil Jeřábek Jan 14 '13 at 12:06
On second thought: the schema I wrote, while being a consequence of ZFC, is a bit stronger than $N$, as the satisfaction predicate for $V_{\omega+\omega}$ is not itself definable in $V_{\omega+\omega}$. A correct axiomatization consists of all implications $\mathrm{Prov}_{\mathrm{ZFC}\restriction n}(\ulcorner\phi^{V_{\omega+\omega}}\urcorner)\to\phi^{V_{\omega+\omega}}$, where $\phi$ is a sentence and $n\in\mathbb N$, and $\phi^{V_{\omega+\omega}}$ denotes relativization of quantifiers. (Note that this is a polynomial-time computable set of axioms.) – Emil Jeřábek Jan 14 '13 at 13:03