A fully satisfactory logical language should be capable of representing any pattern of dependence and independence between variables. In the usual logical languages, dependencies between variables are expressed by dependencies between the quantifiers to which they are bound, while dependencies between quantifiers are expressed by the nesting of their scopes. But in the received first-order logic such nesting does not allow us to express arbitrary patterns of dependence and independence. Hence the received first-order logic has to be extended to IF first-order logic.
One particularly interesting kind of pattern involves interdependence. Sequences of interdependent variables can be thought of as vectors in a logical space. Then the set of all Skolem functions of a given sentence defines an operator (Skolem operator), i.e. a mapping of that space into itself. The sentence S states that those and only those vectors exist that are eigenvectors of one of the Skolem operators of S. In the logic of interdependent quantifiers, instantiation becomes tricky and in some cases impossible. All this is relevant to the applications of IF logic.