 Let us denote by \(\mathbf{FPO}\) the logic of finite partially ordered quantifiers obtained from first-order logic as follows: if \(\phi\) is a first-order formula and \(\mathbf{Q}\) is a finite partially ordered quantifier, then \(\mathbf{Q}\phi\) is a formula of  \(\mathbf{FPO}\).[9]  With \(\mathbf{FPO}\) it is possible to express properties that are not definable in first-order logic. The first example was provided by Andrzej Ehrenfeucht (cf. Henkin 1961): a sentence that is true in a model iff the size of its domain is infinite. It turns out that \(\mathbf{FPO}\) can be translated into IF logic (see Subsect. 4.1). Therefore IF logic is more expressive than first-order logic.