Caveat: All of this is essentially philosophy at this point and so there's no rigorous argument I can present that second-order logic is wrong. But I think you've asked reasonable questions so let's dive in.

So the CH statement (let's call it CH_2 where 2 is for second-order) I was referring to actually uses the empty vocabulary (i.e. only the usual symbols from second-order logic). In particular that means it also applies to second-order Peano Arithmetic.

So does your model of the natural numbers satisfy CH_2 or not (or put differently, is your proposed model of the natural numbers actually a model of the natural numbers)? Depends on your metatheory.

More problematically, what this demonstrates (because CH is independent of ZFC) is that second-order logic loses the absoluteness of semantic truth. That is the statement "M is a model of my theory T under a given interpretation I" can flip-flop between true and false and back again as you continue to expand your background model of your metatheory (think of e.g. Cohen forcing).

So while you may have specified exactly one model, it's getting pretty hard to see just exactly which one it is.

First-order logic does not have this phenomenon, which is why we can often get away with not going into too much detail about our metatheory in FOL (and why recursive metatheories built of FOL "all the way down" aren't too problematic). If M is a model of T under I then it will continue to be a model of T under expansion of my background model. So as long as I sketch out the basics of my metatheory (and by implication my background model), I know I'm good.

Philosophically this means that in the realm of SOL the only way you can be sure that you've really got "the" standard model and haven't mistakenly grabbed another one is if you can confidently state the truth value of every one of a never-ending stream of theorems which cannot be proved using your metatheory.

Indeed statements like "Theorem A is independent of theory T" are very murky and difficult to understand in a second-order setting. For example, CH_2 is definitely not provable using second-order PA, but does that mean we can accept systems with either CH_2 or Not(CH_2)? Well that seems to be false if we take "a single canonical model" at face value, which would imply that only one of the two can be "true," but then how do you decide whether to accept CH_2 or Not(CH_2)? No syntactic argument will suffice since we've lost completeness.

That's not to say I think that second-order logic has no value. I think second-order logic, interpreted using first-order semantics, is a valuable language. However, I agree very much with Vaananen's contention that in practice, SOL reduces to multi-sorted FOL.

> if second-order logic is used in formalizing or axiomatizing mathematics, the choice of semantics is irrelevant: it cannot meaningfully be asked whether one should use Henkin semantics or full semantics. This question arises only if we formalize second-order logic after we have formalized basic mathematical concepts needed for semantics. A choice between the Henkin second-order logic and the full second-order logic as a primary formalization of mathematics cannot be made; they both come out the same.

http://www.math.helsinki.fi/logic/people/jouko.vaananen/VaaS...