5
$\begingroup$

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.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
9
$\begingroup$

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.

Improve this answer
$\endgroup$
6
  • 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
    Commented Sep 18, 2010 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
    Commented Sep 19, 2010 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
    Commented Sep 19, 2010 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
    Commented Sep 19, 2010 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
    Commented Sep 20, 2010 at 15:21

You must log in to answer this question.