[Tainnor]

> However, my understanding is that the incompleteness results apply to only recursively enumerable axiomatic systems. I can find references for this.

That's a matter of semantics as to what you consider the first incompleteness theorem to be precisely (of which there are several variants). Gödel's proof itself doesn't directly work for second-order logic. But the statement "if Γ is some axiomatic system that satisfies certain conditions, then for any sound proof calculus there is a sentence that isn't provable from Γ in this calculus" is true in second order logic too, it's just that the "failure" happens much "earlier" (and is in some sense obvious) than in the case of FOL.

> PA_2 is not such a system and as such the Incompleteness Theorems don’t apply.

I'm really not all that familiar with second-order PA, but it is my understanding that the set of its axioms is decidable. It consists of a finite collection of axioms plus one schema (comprehension axiom) which is valid when it's instantiated by any given sentence - but deciding whether something is a valid sentence is easy. Therefore, what you quoted applies to second-order PA too.

[gedpeck]

From what you and the other person on this thread has said and from what I've read it appears that perhaps the following is true:

1. The axioms of PA_2 are recursively enumerable. 2. The full semantics of PA_2 are what cause categoricity.

It seems to me then that the crux of the matter is that the full semantics of PA_2 prevent there being an effective deductive system. I think Z_2 is constructed to get around the non effectiveness of the full semantics of PA_2 and is a weaker theory.

Anyway, thanks for the enlightenment.

[Tainnor]

With the caveat that I don't really understand second order logic well enough to say all that much about it, there's a debate in the philosophy of mathematics as to whether second-order logic should count as the foundational logic, since on the one hand most first-order theories aren't categorical (due to Löwenheim-Skolem) and on the other hand, second order logic (with full semantics) already presupposes set theory.

In any case, the reason why PA_2 is categorical is because the second-order axiom of induction allows quantification over arbitrary sets which allows you to say that "0 and adding the successor function to 0 arbitrarily often already gives you all natural numbers".