 As it occurs in every higher-order logic, completeness and compactness fail for sort logic with standard semantics. Fortunately, it is possible to build a Henkin structure satisfying both Comprehension axioms and to move to general semantics. Changing semantics in this way results in the recovery of completeness for the mentioned calculus, as Väänänen (2014: 179–80) has remarked. The proof found its inspiration in that of Henkin’s (1950) for type theory.