3
$\begingroup$

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

Improve this question
$\endgroup$

2 Answers 2

Reset to default
3
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • 2
    $\begingroup$ 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. $\endgroup$
    – Carl Mummert
    Commented Mar 27, 2012 at 12:19
  • $\begingroup$ 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. $\endgroup$
    – abo
    Commented Mar 27, 2012 at 18:06
  • $\begingroup$ math.stackexchange.com/q/23799/468 $\endgroup$
    – Kaveh
    Commented Apr 18, 2012 at 3:29
7
$\begingroup$

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

Improve this answer
$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – Lucas K.
    Commented Mar 26, 2012 at 23:29
  • 11
    $\begingroup$ @Lucas K.: "second-order arithmetic", and in particular $ACA_0$, is a first-order theory. $\endgroup$
    – Carl Mummert
    Commented Mar 26, 2012 at 23:31

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .