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?
$\begingroup$
$\endgroup$
3
-
$\begingroup$ If its helpful to know, second order arithmetics is a first order theory. The set variable are not actually second order variables. Usually the language would include a unary predicate that indicates something is a "set". $\endgroup$– WilliamCommented Aug 3, 2012 at 3:15
-
3$\begingroup$ I'm not sure I understand the question. On the one hand, it seems to me semantically impossible to have, say, a model of seventh-order arithmetic in which the seventh-order variables were well-ordered: what would this well-ordering consist of? On the other hand, given $n$, I can take a well-founded model $M$ of $V=L$ and look at the first $n$ many powersets of $\omega$. It seems to me that this gives a model of $n$-th order arithmetic in which the first $n-1$ many sorts are well-ordered. Am I understanding the question correctly? $\endgroup$– Noah SchweberCommented Aug 3, 2012 at 3:25
-
$\begingroup$ William, yes people often say things like "axiomatic second order arithmetic $Z_2$ is a first order theory." Yet $Z_2$ is still widely called second order arithmetic. So I tried to be clear that I am asking about an axiomatic theory with stated axioms and not about what people call the full second order semantics. Noah, yes what you say is right. So my question is what does it take to get an inner model of $V=L$ in $Z_n$ without recourse to ZF. $\endgroup$– Colin McLartyCommented Aug 3, 2012 at 12:51
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
1
There is quite a bit of this in Simpson's book Subsystems of Second Order Arithmetic in the specific context of second-order arithmetic. Here are three relevant results:
Corollary VII.5.11 (conservation theorems). Let $T_0$ be any one of the $L_2$-theories $\Pi^1_\infty\text{-CA}_0$, $\Pi^1_{k+1}\text{-CA}_0$, $\Delta^1_{k+2}\text{-CA}_0$, $0 ≤ k < \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.
Here $\Pi^1_\infty\text{-CA}_0$ has the full comprehension scheme for second order arithmetic, and hence also the full induction scheme.
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:
- $\Sigma^1_{k+3}\text{-AC}_0$ is equivalent to $\Delta^1_{k+3}\text{-CA}_0$.
- $\Sigma^1_{k+3}\text{-DC}_0$ is equivalent to $\Delta^1_{k+3}\text{-CA}_0$ plus $\Sigma^1_{k+3}\text{-IND}$.
- Strong $\Sigma^1_{k+3}\text{-DC}_0$ is equivalent to $\Pi^1_{k+3}\text{-CA}_0$.
- $\Sigma^1_\infty \text{-DC}_0$ ($=\bigcup_{k < \omega} \Sigma^1_k\text{-DC}_0$ ) is equivalent to $\Pi^1_\infty\text{-CA}_0$.
and
Corollary IX.4.12 (conservation theorem). For all $k <\omega$, $\Sigma^1_{k+3}\text{-AC}_0$ (hence also $\Delta^1_{k+3}\text{-AC}_0$ ) is conservative over $\Pi^1_{k+2}\text{-CA}_0$ for $\Pi^1_4$ sentences.
answered Aug 3, 2012 at 3:49
-
$\begingroup$ Thank you. Im not sure with the sub/superscripts, does this imply countable AC, thus the Rasiowa-Sikorski lemma ? If so does how does that relate to forcing proofs relying on this lemma ? It is often claimed that forcing can be carried out in weak theories of arithmetic, but it seems to me that that is only true for formal presentations of those proofs: we prove something like "a forcing proof of independence of CH from ZFC can be described in arithmetic by predicates on Gödel numbers of set theory formulas" - any universal theory should do. Actual forcing requires a set theory with infinity. $\endgroup$– plmCommented Oct 9 at 18:19