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



How do you restrict the induction axiom in second (or higher) order logic?
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. 


