 In fact, any calculus for one-sorted first-order logic can be easily extended to a many-sorted one; the only rules which need to be adapted are the ones dealing with quantifiers and substitution, as they have to take into consideration the variety of sorts admitted. In the entry  classical logic  the rules that need to be changed are: introduction and elimination of universal quantifier (\(\forall \mathbf{I}\) and \(\forall \mathbf{E}\)), introduction and elimination of existential quantifier (\(\exists \mathbf{I}\) and \(\exists \mathbf{E}\)) as well as the rules dealing with equality (\(=\mathbf{I}\) and \(=\mathbf{E}\)).