 Schönfinkel’s aim was to minimize the number of logical constants that are required for a formalization of FOL, just as Henry M. Sheffer (indeed, already Charles S. Peirce) did for classical propositional logic. One of the two quantifiers mentioned above suffices and the other may be assumed to be defined. Let us say, \(\exists x A\) is an abbreviation for \(\lnot\forall x\lnot A\). Even if \(\lnot\) and the rest of the connectives are traded in for \(\mid\), two logical constants remain: \(\forall\) and \(\mid\).  A further pressing issue is that quantifiers may be nested (i.e., the scope of a quantifier may fully contain the scope of another quantifier), and the variable bindings (that could be visualized by drawing lines between quantifiers and the variables they bind) may get quite intertwined. Keeping for a moment the familiar logical constants, we may look at the following formula that hints at the emerging difficulties—when the question to be tackled is considered in its full  generality.[2]