There are statements $\varphi$ that are independent of first-order Peano Axioms. Are these statements also independent of second-order Peano Axioms?
I'm reading Wikipedia articles around independence results and it has come evident that the second-order formulation of PA is strictly more powerful than first-order formulation. I don't, however, see if this has any connection to independence results.
In first-order logic, there is a complete equivalence between provability and logical validity (truth in all models); this is known as Goedel's completeness theorem. Theories such as first-order Peano arithmetic (PA) have many models, including the standard one and many non-standard ones. Each independent sentence is true in some models and false in others, and in fact this is what causes a sentence to be independent, because if a sentence was true in every model it would be provable and if it was false in every model it would be disprovable.
Second-order logic can be studied with two semantics, "full" and "Henkin". In "full" semantics, there is only one model of a particular theory $PA_2$ of second-order arithmetic, and this model consists of the standard natural numbers $\mathbb{N}$ along with all subsets of $\mathbb{N}$. In Henkin semantics, the same theory $PA_2$ has many models, and these models do not all make the same sentences true.
There is a standard deductive system for second-order arithmetic which is called $Z_2$. It consists of the axioms for $PA_2$ along with a comprehension scheme which states that each set of the form $\{n \in \mathbb{N} : \Phi(n)\}$ exists, where $\Phi$ is a formula of second-order arithmetic with parameters. The system $Z_2$ is sound in both full and Henkin semantics, when the appropriate class of Henkin models is used. In particular, from a syntactic viewpoint, the deductive system $Z_2$ can be viewed as a consistent, effectively generated formal system that includes a large amount of arithmetic. Thus, because Goedel's incompleteness theorem applies to all such systems, there must be sentences that are true in the standard model of (first-order) arithmetic which are not provable in $Z_2$ (nor disprovable, because $Z_2$ is satisfied by the standard model). The only role of the semantics here is to verify that $Z_2$ is consistent; apart from that the semantics are irrelevant to the conclusion that $Z_2$ is syntactically incomplete. Also, the independent sentences are still first-order, and in fact $\Pi^0_1$, just like all sentences obtained from the incompleteness theorem.
The only commonly studied extensions of $Z_2$ include additional schemes corresponding to the axiom of choice. Everything in the previous paragraph also holds, mutatis mutandis, for these extensions. Any consistent, effective formal system including Peano arithmetic has to be syntactically incomplete, even if it can be made semantically complete through a choice of a very strong semantics.
The general theorem here is that there is no effective, sound, and syntactically complete axiom system for second-order logic under full semantics. This is because $PA_2$ is categorical under full semantics, and its only model has the standard natural numbers. Thus any such system could be used to effectively enumerate the set of formulas of Peano arithmetic that are true in $\mathbb{N}$, which is impossible because the set of such formulas is not computably enumerable.
In general, there is a tradeoff between the strength of the semantics and the completeness of the deductive system. If you tighten the semantics (by allowing fewer models), as with full second-order semantics, you may gain categoricity of theories but lose completeness of the deductive system. If you loosen the semantics (allowing more models) you may gain completeness of the deductive system but lose categoricity results.
When we study second-order arithmetic, we typically use Henkin semantics, because these are much more amenable to mathematical analysis than full second-order semantics.
Now, looking the other way, we can ask whether every sentence $\phi$ that is independent of first-order Peano arithmetic is also independent of $Z_2$. The answer to that is no. For example, the Goedel sentence Con(PA) for Peano arithmetic is provable in $Z_2$. Here is a proof sketch. First, $Z_2$ has enough comprehension axioms to ensure that every model of $Z_2$ contains a truth function for first-order formulas. In any particular model of $Z_2$, this function takes a formula of Peano arithmetic and returns T or F depending on whether that formula is true or false about the numbers in that model. $Z_2$ proves that every axiom of Peano arithmetic is sent to T by this function and that the truth value T is preserved by the inference rules of Peano arithmetic. Thus, by induction, $Z_2$ proves that no deduction in Peano arithmetic can conclude with $0=1$ because that formula is sent to F in every model of $Z_2$. The key point is the construction of the truth function, uses comprehension for a non-first-order formula. It would not be possible to construct a function in $Z_2$ that tells whether an arbitrary formula of second-order arithmetic is true or false.
