# First Order Predicate Logic with only one operator?

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))$$

(That ‽ 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.

• Interesting! My first time hearing about "nextand". Reminds me of Cylindric algebra I guess automated theorem proving might be a potential area of application, although currently type theory seems to be dominating there. – Thinking Torus Apr 14 at 7:05