 As mentioned already, in Henkin 1953 a new calculus for second order logic was defined by eliminating some Substitution Rules from the calculus presented in Church  1956[20]  and introducing Comprehension Schema. In this paper, Henkin defines two calculi \(F^{\ast}\) and \(F^{\ast \ast}\) (basically, calculi MSL and SOL): the first one is obtained from a first-order calculus by adding rules for the new quantifiers, while the second is a proper second-order calculus. Both calculi are incomplete with standard semantics. Henkin mentioned that we can obtain a completeness result for the \(F^{\ast}\) calculus with the frame semantics. In fact, we have already seen completeness for MSL and that the second-order calculus is complete with the general semantics.