 Thus internal categoricity means categoricity not only for ordinary models, i.e., full Henkin models, but categoricity inside an arbitrary Henkin model. Note that categoricity is a meta-theoretical concept as it refers to the semantics of second-order logic. In \(\categ(\theta(P))\) the categoricity of \(\theta(P)\) is written in the language of second-order logic. That is, the categoricity, despite being a meta-theoretical concept, is written in the object language. It can be asked, whether this leads us to a different concept? Be that as it may, when the meaning of \(\categ(\theta(P))\) is uncovered by considering its semantics in the meta-theory, the meaning is the same as the meaning we give to the categoricity of \(\theta(P)\). In the concept of internal categoricity we take advantage of this situation by switching from semantical meaning to proof-theoretic meaning. We insist that \(\categ(\theta(P))\) is (not only valid but even) provable. Proof-theory requires less meta-theory than semantics. We can investigate provability of second-order sentences even in number theory by using numbers to code sentences and proofs, as Gödel did in his proof of the Incompleteness Theorem. Of course, the Completeness Theorem brings us back to the semantics.