How do you restrict the induction axiom in second (or higher) order logic? Dear all,
I am interested in reverse mathematics. The theory is that most of mathematics can be expressed and proven in ACA0, that is second order logic, with the induction axiom restricted.
However, maybe a stupid question, but how do you restrict the induction axiom in second order logic? If you have the successor function, then the natural numbers can be defined as the closure on that functions. From that definition, if I am not mistaken, the induction axiom follows. So, in fact you do not really have an induction axiom, but you just derive it.
But if it is not an axiom, how do you restrict it?
Regards,
Lucas
 A: You wrote "If you have the successor function, then the natural numbers can be defined as the closure ...".  This definition of the natural numbers presupposes either enough set theory to define the notion of "closure" or a logic that goes beyond first-order logic by having  "closure" (or something similar) built in.  So in a set theory, like ZFC, you can indeed define the natural numbers as you suggest.  In $ACA_0$ and similar theories, however, "natural number" is taken as a primitive notion.  
$ACA_0$ includes the full induction axiom in the form "every set that contains 0 and is closed under successor contains all natural numbers."  Nevertheless, this is a restricted form of induction.  The reason is that, in order to infer the usual induction principle in the form "If $\phi(0)$ holds and if, for all $n$, $\phi(n)$ implies $\phi(n+1)$, then, for all $n$, $\phi(n)$," one needs the additional fact that there is a set of all natural numbers $n$ that satisfy $\phi(n)$, because one needs to apply the induction axiom to this set.  $ACA_0$ provides the existence of such a set only for arithmetical formulas $\phi$, i.e., formulas in which the quantified variables range only over natural numbers.  So the induction principle is available only for arithmetical $\phi$.
A: ACA0 does not merely restrict the induction axiom.  It also restricts the comprehension axiom, which asserts the existence of the second-order entities, to formulae which contain no quantification over big (second-order) letters, that is comprehension in ACA0 is:
(there exists X)(for all n)(n in X iff phi(n)),
where phi(n) contains no quantifiers with big (second-order) letters.
To define the natural numbers N in second-order logic, you would use phi(n) as
(F)(F0 & (x)(y)(Fx & Sx,y implies Fy) implies Fn).
But this obviously has a big-letter quantified, so this definition cannot be made in ACA0.  This is why, as Andreas points out, you assume the existence of N - because it cannot be defined.  
