According to this Wikipedia article the second order axiom of induction is: $$\forall P(P(0)\land \forall k(P(k) \to P(k+1)) \to \forall x(N(x) \to P(x))$$
Where N(x) means x is a natural number. That x is a natural was implied in the article so I added it into the axiom to make it explicit. This axiom is also given informally along with the rest of the Peano axioms here.
Now what the Wikipedia article for Peano arithmetic claims is that "The intuitive notion that each natural number can be obtained by applying successor sufficiently many times to zero requires an additional axiom, which is sometimes called the axiom of induction." However, this claim appeared at first to me to be false.
My reasoning went like this. The material conditional $\to$ does not mean that what is to the left of it logically entails what is to the right of it. For instance $A \to B$ does not mean "A logically entails B." In a logical proof $A \to B$ is a premise precisely because it is not logically self-evident.
Likewise, $P(0)\land \forall k(P(k) \to P(k+1))$ may imply that $\forall x(N(x) \to P(x))$ in terms of truth tables, but this does not mean that the first statement logically entails the second. This means that non-standard models may still exist as long as the first statement is false or the second statement is true, since $A \to B \equiv \lnot A \lor B$. Consider the case where the property P is true for all of the standard natural numbers (so the antecedent is true) and P is also true for all standard natural numbers as well as some non-standard natural numbers in N (the consequent is true). Every P that applies to all standard natural numbers may also apply for all non-standard natural numbers. Then the axiom is affirmed for all P and yet there remain non-standard models.
I suspect what is happening here is that in second order logic, P(a) is interpreted to mean $\exists x \phi$ $(x:=a)$, where $\exists x \phi$ is the "sentence", of which a is the "subject" and everything stated about a in the formula is the "predicate" P. Assuming this, $\forall P$ is interpreted to mean "for all possible formulas $\phi$, when a, b, ... is substituted into them, the following formula $\psi$ is true, if P(a), P(b) ... denotes $\exists x \phi$ $(x:=a)$, $\exists x \phi$ $(x:=b)$" In this case second order quantification is quantifying over all possible formulas that could be applied to some variable(s). Of course with the caveat that these theoretical formulas could be infinitely long, whereas written formulas can only be finite.
In this case the axiom of induction is stating that every possible formula for which the antecedent is true implies the consequent is true. Since every possible formula would include every possible truth assignment for natural numbers as well as non-standard natural numbers, then it includes the formula whose truth assignment is only true of the standard natural numbers. Importantly, it is assumed that all possible P includes the P which applies only to the standard model. If all P in "the set of all possible P" could have the same truth assignments, then it would be the same as first-order logic in terms of expressiveness.
Is this basically correct?
