 The first stage in Schönfinkel’s extension of FOL is analogous. The addition of \(\mid^-\) is (also) a conservative extension of FOL, and every occurrence of \(\mid^-\) can be eliminated. (We noted that \(\mid^-\) is a binary operator, and so it may be thought to combine a quantifier (\(\exists\)) with connectives (\(\lnot\), \(\land\)), but \(\mid^-\) of course, does not introduce any objects that are not definable in FOL.)