 It is useful to have a notation for “nextand” (i.e., “not-exists-and”) without assuming either that \(x\) has a free occurrence in the expressions joined, or that if it has one, then it is the last component of the expressions. Following Schönfinkel, we use \(\mid^x\) for the “nextand” operator that binds \(x\). (The  notation \(\mid^-\), where \(^-\) is the place for a variable, closely resembles the Sheffer stroke.) Schönfinkel achieved his goal of the reduction of the set of logical constants for FOL to a singleton set \(\{\mid^-\}\), because every formula of FOL is equivalent to a formula that contains only “nextand.”