 The completeness proof for a many-sorted calculus could be done by following the well known Henkin (1949) strategy for first-order logic. The important issue is to be able to show that each consistent set of formulas has a model, and hence syntactic consistency and semantic satisfiability are equivalent (assuming Soundness). The proof is performed in basically two steps: