 In fact, with the semantics of frames, the set of validities coincides with the set of sentences derivable in a second-order calculus which is just an extension of the first-order one obtained by adding rules for the new quantifiers. This many-sorted calculus was isolated by Henkin (1953) in a paper where he introduced the Comprehension Schema