 In many-sorted logic the connectives are standard and, therefore, we use the classical definition of satisfaction for formulas built on them. For quantified formulas such as \(\exists x^{i}\varphi\) the definition reads: \(\mathcal{A},s\models \exists x^{i}\varphi\) if and only if there is an \(\mathbf{x}\in \mathbf{A}_{i}\) such that \(\mathcal{A},s(\mathbf{x}/x^{i})\models \varphi\).