 Dependency patterns between quantified variables in first order logic are necessarily transitive, as it is made evident by their connections with the scopes of the corresponding sub-expressions: if \(\exists y\) is in the scope of \(\forall x\) and \(\exists z\) is in the scope of \(\exists y\) then necessarily \(\exists z\) will be in the scope of (and, therefore, dependent from) \(\forall x\). Furthermore, the set of all quantifiers in whose scope some subformula \(\alpha\) lies is linearly ordered: if \(\alpha\) is in the scope of \(Q_1 x_1\) and \(Q_2 x_2\), then either \(Q_1 x_1\) is in the scope of \(Q_2 x_2\) or vice versa.