 Second-order logic satisfies the Completeness Theorem if Henkin models are used. Thus semantic arguments in second-order logic can be turned into syntactic formal proofs, but as with set theory the semantic argument has to be valid in all Henkin models, not only in all of the full Henkin models. Thus, as in set theory, the semantic argument cannot use properties of the Henkin models that are not shared by all Henkin models, In particular, fullness (see  §9.1)  cannot be assumed because in general models it is not a second-order property. What happens to categoricity when fullness is abandoned? We still have internal categoricity, so we can use categoricity in proofs as long as we make sure we work inside one model. One certain way to make sure of this is that we base everything on the axioms, the Comprehension Axiom Schema and the Axioms of Choice.