Let bigset(X) and rel(X,Y) be otherwise arbitrary formulas in the language of second-order arithmetic with the indicated variables free, and thmemberof(Z,x,X) be the formula asserting that X is the xth member of the sequence of sets coded by Z. Does it follow that second-order arithmetic proves

$((\exists X)(bigset(X)) \; \land \; (\forall X)(bigset(X) \implies (\exists Y)(bigset(Y) \; \land \; rel(X,Y)))) \implies$
$(\exists Z)(\forall x)(\exists X)(\exists Y)($
$bigset(X) \; \land \; bigset(Y) \; \land \; thmemberof(Z,x,X) \; \land \; thmemberof(Z,\operatorname{S}(x),Y) \; \land \; rel(X,Y))$


By second-order arithmetic, I mean Robinson arithmetic + full comprehension + the second-order induction axiom.


Carl has pointed out that my previous answer missed a clause in the theorem I cited.

Simpson's book, Subsystems of Second Order Arithmetic, does address this in section VII.6. He shows that dependent choice for $\Sigma^1_2$ formulas is equivalent to $\Delta^1_2$ comprehension plus $\Sigma^1_2$ induction (Theorem VII.6.9).

However even regular (non-dependent) $\Sigma^1_3$ choice is independent of full comprehension; he attributes this result to Feferman and Levy, and cites Theorem 8 of Levy's "Definability in axiomatic set theory, II".

The result I mentioned before, that $\Sigma^1_k$ dependent choice is equivalent to $\Delta^1_k$ comprehension plus $\Sigma^1_k$ induction for $k\geq 2$, holds for $k\geq 3$ requires the additional assumption that the universe is constructible from from some set of integers.

Your statement of dependent choice is a bit more complicated than necessary; you can fold bigset into rel (take $rel'(X,Y)$ to hold if either $\neg bigset(X)$ and $bigset(Y)$, or if $bigset(X)$, $bigset(Y)$, and $rel(X,Y)$). Conversely, it's a bit simpler than the version Simpson uses (which I believe is standard), in which $rel$ can depend on the parameter $x$ as well.

  • 2
    $\begingroup$ Section VII.6 of Simpson's book is particularly terse, and I have always found it hard to read. Theorem VII.6.16 has the extra assumption that $V = L(X)$ for some set $X$. Remark VII.6.3 explains that even $\Sigma^1_3-\mathsf{AC}_0$ cannot be proved in $Z_2$. $\endgroup$ – Carl Mummert Sep 18 '10 at 19:29
  • $\begingroup$ By "the universe" and 'V', do you guys mean Z_2's universe, and then adding that as an additional axiom to Z_2 ? $\endgroup$ – user5810 Sep 19 '10 at 1:34
  • $\begingroup$ Yes. Although second-order arithmetic cannot formalize arbitrary set theory (obviously), it is able to formalize a surprising amount of it. In particular, many properties of the constructible hierarchy $L$ can be formalized in ATRo, and there is a formula $\Phi(X,Y)$ in the language of second-order arithmetic that says that $Y$ is in $L(X)$. So the axiom $(\exists X)(\forall Y)[Y \in L(X)]$ "says" that $V = L(X)$ but of course you are right that it only refers to the portions of $V$ and $L$ that are formalized in second-order arithmetic. $\endgroup$ – Carl Mummert Sep 19 '10 at 12:01
  • $\begingroup$ At first I was thinking the theorem was "If V=L(X), then Z_2 proves every instance of Dependent Choice" before I remembered that every arithmetical sentence provable in ZF+V=L(X) is provable in ZF, though I asked to make sure my new understanding was correct. Also, what is AC_0 ? $\endgroup$ – user5810 Sep 19 '10 at 22:17
  • $\begingroup$ \Sigma^1_3-ACo is a subsystem of second order arithmetic consisting of ACAo plus the axiom of choice for \Sigma^1_3 formulas. The subscript 0 indicates limited induction. Also, the result you allude to (Shoenfield's absoluteness theorem) only works up to the Sigma^1_2 level. This suggests that Sigma^1_3 is the first case that could be problematic, which it is. Not every sentence in the language of second-order arithmetic is arithmetical (= in the arithmetical hierarchy). $\endgroup$ – Carl Mummert Sep 20 '10 at 15:21

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.