Question: 2-logics quantify over predicates, 3-logics over predicates of predicates and so on.

Unlike 1-logic where we have nice meta-logical properties of soundness, completeness & effectiveness - these properties fail for higher logics.

But they're reobtained if instead of using full semantics we use Henkin semantics where the quantifiers are bounded. This means they reduce to typed 1-logic.

Consider the statement: Beethoven has all the properties that make for a great musician.

Surely, here one needs to restrict to properties that are applicable to human beings and not say to the moon for example?

Does this mean that typed 1-logic is more natural than just 1-logic? We have nice meta-logic properties, plus the expressibility of higher logics. 

For example stating the least upper bound property for the reals is not possible in 1-logic, but it is in 2-logic.

Is there a strong argument for considering 1-logic more fundamental than typed 1-logic?

Answer: 
Henkin semantics is equivalent to first-order logic + comprehension schema in expressive power. So if there's any reason to accept Henkin semantics over first-order logic, it will be insofar as one takes the comprehension schema to be logical truths.

There's a subtlety in the interpretation of these schema, viz. the quantified predicate variables are better thought of as *sets* as opposed to *properties*. So for instance, the sentence "Beethoven has all the properties that make for a great musician," if schematized in second-order logic, would say (roughly) "Beethoven is in every set that every great musician is in", or equivalently "Beethoven is in the set of great musicians," which doesn't quite have the intended meaning you suggested.

Perhaps this may make the comprehension schema look more plausible. But even if they're *true*, that doesn't yet mean they are *logically true*. Similarly, "Beethoven has all the properties that make for a great musician" doesn't yet give us reason to adopt Henkin semantics over, say, full semantics. For while it's *natural* to assume these properties are human properties (technically, the quantifiers range over the power set of the set of humans), that may not be something which is determined by our *logic*. If anything, our logic should be *neutral* to whether or not these properties being referred to are ones that only apply to humans (surely it's *logically* possible for the moon to sing, right?). But now, for comprehension schema, if they're true, are they true by virtue of logic? That will depend on your view regarding more fundamental philosophical issues.
Henkin semantics is important for higher order logic, but keep in mind that it is not automatically fully specified in every situation. Especially, are there any comprehension axioms at all, and if there are comprehension axioms, should they be predicative (i.e. avoid "inner" quantification over higher order variables) or impredicative (i.e. using arbitrary formulas including quantification over higher order variables as if they were first order variables).

Also note that the comprehension axioms can have a sort of "last word" property, i.e. if you introduce additional non-logical symbols into the language, all additional comprehension axioms enabled by these additional symbols become immediately available. Worse still, consider that the context of the logic can be extended to include Henkin quantifiers, cardinality quantifiers (or "nasty" transfinite quantifiers) or forms of infinitary logic (since we must assume an underlying set theory anyway). But all this additional expressivity of the language is automatically available for the comprehension axioms too. (I'm not so sure about impredicative comprehension axioms here, since they might quickly lead to paradoxes in case the language is extended beyong pure first-order logic.)

On the other hand, consider also the case where quantification over higher order variables is nearly absent, like in pure propositional logic where one just has a formula including propositions, and just want to know whether the formula is satisfiable (corresponding for existential quantification over all propositions), or whether the formula is a tautology (corresponding to universal quantification over all propositions). If we treat unquantified higher order variables in the same way, will standard semantics actually be different from Henkin semantics?