Axiom schemas, such as the PA induction schema, differ from second-order axioms in that they only hold for "definable" predicates, rather for "all" predicates. As a result, you can have non-standard models of first-order PA for which induction holds for all definable predicates, but does not hold true in general.
This leads to questions about which predicates "exist." In general, for every possible infinite combination of natural numbers (or more generally, objects in the domain), is there considered to "exist" a unary predicate that is "true" for only those numbers, even if the predicate is undefinable? And likewise with n-ary predicates?
This would seem to be a semantic thing. Is there an "axiom of first-order logic" that determines which of these predicates we consider to "exist?" (Or would this perhaps be more pertinent to second-order logic, being related to things like Henkin semantics?)
Best Answer
The answers are different syntactically and semantically. We can stick to second-order arithmetic here, but second-order logic in general acts the same.
Semantically, if we work with "full models" then, in each model, we require the second-order part to include all subsets of the first order part. If the model also satisfies the induction axiom $$ \forall A( 0 \in A \land (\forall n)[n \in A \to n+1 \in A]) $$ then the model will satisfy induction for every subset of the first-order part (which, in conjunction with a few other first-order axioms, will force the first-order part to be the standard natural numbers $\omega$).
If we work with "Henkin models" then we allow the second-order part to be a proper subset of the first-order part. The set-existence axioms in the theory then determine which sets of first-order objects must be in the model. But even with the strongest set existence schemes we will not ensure that all subsets of the first-order part are included.
The difference is not so significant when we work syntactically and look at formal proofs instead of models. When we consider full second-order logic syntactically, we often view the set existence axioms as "part of the logic", because our choice of models forces the set existence axioms to hold. But, even though our models now must contain all subsets, in a formal proof we can still only construct some of them - the ones that come from the set existence axioms. So, when we work syntactically, we are essentially in the same position if we look at full models or at Henkin models.