Does higher order arithmetic interpret the axiom of choice? - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-24T20:42:23Z http://mathoverflow.net/feeds/question/103835 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/103835/does-higher-order-arithmetic-interpret-the-axiom-of-choice Does higher order arithmetic interpret the axiom of choice? Colin McLarty 2012-08-03T02:55:58Z 2012-08-03T03:49:03Z <p>By second order arithmetic I mean the axiomatic theory $Z_2$, that is Peano arithmetic extended by second order variables with the full comprehension axiom, and not defined semantically using power set in ZF. By third order arithmetic I mean that extended by third order variables and the comprehension axiom. And so on. Does each of these have an inner model which also satisfies the axiom of choice in each order, using constructibility? If not, do such inner models exist if we also extend induction to a higher order axiom? Is there a good reference on it? </p> http://mathoverflow.net/questions/103835/does-higher-order-arithmetic-interpret-the-axiom-of-choice/103839#103839 Answer by Carl Mummert for Does higher order arithmetic interpret the axiom of choice? Carl Mummert 2012-08-03T03:49:03Z 2012-08-03T03:49:03Z <p>There is quite a bit of this in Simpson's book <em>Subsystems of Second Order Arithmetic</em> in the specific context of second-order arithmetic. Here are three relevant results:</p> <blockquote> <p>Corollary VII.5.11 (conservation theorems). Let $T_0$ be any one of the $L_2$-theories $\Pi^1_\infty\text{-CA}_0$, <code>$\Pi^1_{k+1}\text{-CA}_0$,</code> <code>$\Delta^1_{k+2}\text{-CA}_0$,</code> $0 ≤ k &lt; \infty$. Let $\phi$ be any $\Pi^1_4$ sentence. Suppose that $\phi$ is provable from $T_0$ plus $\exists X \forall Y (Y ∈ L(X ))$. Then $\phi$ is provable from $T_0$ alone.</p> </blockquote> <p>Here <code>$\Pi^1_\infty\text{-CA}_0$</code> has the full comprehension scheme for second order arithmetic, and hence also the full induction scheme. </p> <blockquote> <p>Theorem VII.6.16 ($\Sigma^1_{k+3}$ choice schemes). The following is provable in $\text{ATR}_0$. Assume $\exists X \forall Y (Y ∈ L(X ))$. Then: </p> <ol> <li><code>$\Sigma^1_{k+3}\text{-AC}_0$</code> is equivalent to <code>$\Delta^1_{k+3}\text{-CA}_0$</code>.</li> <li><code>$\Sigma^1_{k+3}\text{-DC}_0$</code> is equivalent to <code>$\Delta^1_{k+3}\text{-CA}_0$</code> plus <code>$\Sigma^1_{k+3}\text{-IND}$</code>. </li> <li>Strong <code>$\Sigma^1_{k+3}\text{-DC}_0$</code> is equivalent to <code>$\Pi^1_{k+3}\text{-CA}_0$</code>.</li> <li><code>$\Sigma^1_\infty \text{-DC}_0$</code> (<code>$=\bigcup_{k &lt; \omega} \Sigma^1_k\text{-DC}_0$</code> ) is equivalent to <code>$\Pi^1_\infty\text{-CA}_0$</code>.</li> </ol> </blockquote> <p>and</p> <blockquote> <p>Corollary IX.4.12 (conservation theorem). For all $k &lt;\omega$, $\Sigma^1_{k+3}\text{-AC}_0$ (hence also <code>$\Delta^1_{k+3}\text{-AC}_0$</code> ) is conservative over <code>$\Pi^1_{k+2}\text{-CA}_0$</code> for $\Pi^1_4$ sentences.</p> </blockquote>