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?

  • $\begingroup$ So you want something like ZC+PD sort of thing? $\endgroup$
    – Asaf Karagila
    Jan 13, 2013 at 15:18
  • $\begingroup$ Do you mean ZC + Borel determinacy? Would that be sufficient? $\endgroup$
    – arsmath
    Jan 13, 2013 at 16:23
  • $\begingroup$ 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). $\endgroup$ Jan 13, 2013 at 19:59
  • $\begingroup$ 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.) $\endgroup$ Jan 18, 2013 at 20:01

1 Answer 1


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.

  • 1
    $\begingroup$ 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)$.) $\endgroup$
    – arsmath
    Jan 13, 2013 at 17:31
  • $\begingroup$ 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$. $\endgroup$ Jan 14, 2013 at 12:06
  • $\begingroup$ 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.) $\endgroup$ Jan 14, 2013 at 13:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.