 What is gained with the slash notation? After all, clearly e.g. \((\forall x)(\forall y)(\exists z/\forall y) R(x, y, z)\) is true in a model \(M\)  iff[6]  the first-order sentence \((\forall x)(\exists z)(\forall y) R(x, y, z)\) is true therein. As a matter of fact, the expressive power of IF logic exceeds that of first-order logic. Consider the sentence \((\forall x)(\exists y)(\forall z)(\exists w/\forall x) R(x, y, z, w)\). Its truth-condition is of the following form: there are one-argument functions \(f\) and \(g\) such that \(R(a, f(a), b, g(b))\) holds in \(M\), for any \(a\) interpreting \(\forall x\) and \(b\) interpreting \(\forall  z\).[7]  So the sentence is true iff the following sentence (*) containing a finite partially ordered quantifier is true: