 It seems unfortunate that Schönfinkel’s reduction procedure for FOL is not widely known. As a measure of how widely Sheffer’s and Schönfinkel’s reductions are known, we appeal to the fact that the first is part of standard intro courses in logic, whereas the second is not. Undoubtedly, one of the reasons for this is that Schönfinkel’s process to eliminate bound variables is conceptually more opulent than defining a few truth functions from \(\mid\) (or \(\downarrow\)). Another reason may be that Schönfinkel, perhaps, did not place a sufficiently strong emphasis on the intermediate step that allows the elimination of all other logical connectives and quantifiers via “nextand.” The importance of this step was also overlooked in the introduction to the English translation of Schönfinkel’s paper, which was written more than 30 years after the original publication. We may also note that although “nextand” is an operator in the standard logical sense, it is binary—unlike \(\forall\) and \(\exists\), which are unary.