Sketch of the proof
1) We define the syntax for SOL and the corresponding deductive apparatus, adding axioms and rules for managing second-order quantification (see e.g. van Dalen, Logic and Structure (2013), Ch.5).
2) We define the "standard" semantics for the language.
3) We define the concept of standardly valid extending in a natural way the FOL concept.
Then we prove the :
Soundness Theorem : Every theorem of second-order predicate calculus is standardly valid.
4) We consider the FOL version of Peano axioms plus the Axiom of induction; it is important to note that, in the SOL version, Induction is a formula and not an axiom schema.
5) Let AR2 be the conjunction of the first-order axioms of formal arithmetic plus the
second-order axiom of mathematical induction.
We prove that :
Any two standard interpretations M and M' that are models of AR2 are isomorphic.
6) Let L2A the second-order language for arithmetic (with the nonlogical constants of formal arithmetic : zero, successor, addition, multiplication).
Let N be the standard interpretation of L2A with the set of natural numbers as its domain and the usual interpretations of the nonlogical constants.
We prove (using 5) that :
Let B be any formula of the language of arithmetic. Then B is true in N if and only if AR2 ⇒ B is standardly valid.
7) We prove that :
The set SV of standardly valid formulas of L2A is not effectively enumerable.
Assume that SV is effectively enumerable. Then, by 6, we could effectively enumerate the set TR of all true formulas of first-order arithmetic by running through SV, finding all formulas of the form AR2 ⇒ B, where B is a formula of first-order arithmetic, and listing those formulas B. Then the theory TR would be decidable (which is not), since, for any closed formula C, we could effectively enumerate TR until either C or its negation appears.
8) From 7 we have that the set of all standardly valid formulas is not effectively enumerable.
An enumeration of all standardly valid formulas would yield an enumeration
of all standardly valid formulas of L2A, since the set of formulas of L2A is decidable.
9) There is no effective formal system whose theorems are the standardly
valid formulas of L2A.
If there were such an axiom system, we could enumerate the standardly valid formulas of L2A, contradicting 7.
10) Incompleteness of Standard Semantics : There is no effective formal system whose theorems are all standardly valid formulas.
If there were such an axiom system, we could enumerate the set of all standardly
valid formulas, contradicting 8.
The last fact clearly distinguishes second-order logic from first-order logic, since Gödel’s completeness theorem tells us that there is an effective formal system whose theorems are all logically valid first-order formulas.