It's fairly well known that Propositional Logic can be expressed with only one operator -- either the Sheffer Stroke (aka NAND, a dyadic operator written infix as $\vert$); or Peirce's Arrow (aka NOR, written $\downarrow$).
In First Order Predicate Logic, it's also well known that you can dispense with one of the quantifiers, using the equivalences
$$ \exists x. P(x) \equiv \lnot\forall x.\lnot P(x) \\ \forall y. Q(y) \equiv \lnot\exists y. \lnot Q(y) $$
I've just run across a single-operator basis for FOL due to Schönfinkel, using an operator that's a combo of Sheffer Stroke with Existential quant. It's written like a Sheffer Stroke, with the quantified variable superscripted:
$$ P(x)|^xQ(x) \equiv \lnot\exists x.(P(x) \land Q(x)) $$
It seems to be not well known(?) That Stamford Encyclopedia article calls it nextand, but Google doesn't bring up many refs. I'm not sure that's a happy name: my brain wants to read that as 'next-and' and indeed many of the Google hits are to temporal logic 'next-and-until'.
Q 1. Is nextand well-known in the right circles? Does it go under other aliases?
Q 2. Could there be other single operators as a basis for expressing FOL? I'm thinking you could base one on Peirce's Arrow; and/or you could base on universal quant:
$$ P(x)\downarrow^xQ(x) \equiv \lnot\exists x.(P(x) \lor Q(x)) \\ P(x)‽^xQ(x) \equiv \lnot\forall x.(P(x) \land Q(x)) \\ P(x)⸘^xQ(x) \equiv \lnot\forall x.(P(x) \lor Q(x)) $$
‽ I've pulled out of thin air. I've used
⸘ there because mathjax in stackexchange doesn't seem to support '\textinterrodown' or '\textinterrobang' or other exotica.)
Q 3. Is there any reason to prefer one of the four? (I'm guessing any formula using them is going to become unreadable, so this is a purely academic exercise, right?)
The Sheffer Stroke is popular because it corresponds to a NAND gate in electronics.