8
$\begingroup$

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?

Improve this question
$\endgroup$
4
  • $\begingroup$ So you want something like ZC+PD sort of thing? $\endgroup$
    – Asaf Karagila ♦
    Commented Jan 13, 2013 at 15:18
  • $\begingroup$ Do you mean ZC + Borel determinacy? Would that be sufficient? $\endgroup$
    – arsmath
    Commented 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$
    – Rachid Atmai
    Commented 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$
    – Andrés E. Caicedo
    Commented Jan 18, 2013 at 20:01

1 Answer 1

Reset to default
5
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • 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
    Commented 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$
    – Emil Jeřábek
    Commented 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$
    – Emil Jeřábek
    Commented Jan 14, 2013 at 13:03

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .