 An axiomatic calculus for sort logic was introduced in Väänänen (2014), as an extension of the second-order case. For this reason, he incorporated a second Comprehension Axiom related to \(\widetilde{\exists}\) together with some restrictions concerning the rules of proof when formulas with the new quantifier \(\widetilde{\exists }\) are involved (see 2014: 176–177).