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

-

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.

-
A deeper issue is that, as Andreas says, it only makes sense to "define" $\mathbb{N}$ in the context of an ambient set theory. In arithmetic, $\mathbb{N}$ is simply the domain of discourse, and is definable as $\{x:x=x\}$. Separately, even if we have $\Pi^1_1$ comprehension, which can form the set defined by the formula in this answer, that set may not actually be the standard $\omega$, because there are nonstandard models of full comprehension that still satisfy induction for every set in the model. The trouble is that "the closure of a set under a function" is model dependent in FOL. – Carl Mummert Mar 27 '12 at 12:19
I don't agree about the point in the first sentence. In Frege Arithmetic one defines N exactly as I have written it. I don't agree that N is "definable" as the identity set, in any sense in which the original poster was asking his question. – abo Mar 27 '12 at 18:06
math.stackexchange.com/q/23799/468 – Kaveh Apr 18 '12 at 3:29

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$.

-
Note that I was talking about second order logic, and not first order logic. A closure can be defined in second order logic. But I will read your answer more carefully tomorow. – Lucas K. Mar 26 '12 at 23:29
@Lucas K.: "second-order arithmetic", and in particular $ACA_0$, is a first-order theory. – Carl Mummert Mar 26 '12 at 23:31