# Is there a known shorter axiomatization of NF than this?

Is there an already known axiomtization of $$NF$$ that is shorter than the following axiomatic system in first order logic with equality $$="$$ and membership $$\in"$$? And what is exactly meant by shorter is having less total number of symbols in all of its axioms than the total number of symbols in all axioms of this system.

1. Extensionality: as in $$NF$$
2. Complements: $$\forall A \exists x \forall y(y \in x \leftrightarrow y \not \in A)$$
3. Pairing: $$\forall a,b \exists x \forall y(y \in x \leftrightarrow y=a \lor y=b)$$
4. Set union: $$\forall A \exists x \forall y(y \in x \leftrightarrow \exists m \in A (y \in m))$$
5. Frege $$1^*$$: $$\exists x \forall y(y \in x \leftrightarrow\exists z \forall m \in y \ (z=m))$$
6. Product: $$\forall R,S \exists x \forall y (y \in x \leftrightarrow \exists r \in R \ \exists s \in S \\ \forall z \in y \ ( z \in s \lor z \in r))$$
7. Unordered intersection relation set: $$\exists x \forall y (y \in x \leftrightarrow \exists z \forall m \in y (z \in m))$$

The already known finite axiomatizations of $$NF$$ present in literature that I know of are those of Hailperin and Randall Holmes (see here Pages: 7,15), and those are very long compared to the above mentioned one.

• "shorter" in what way? Clearly you can take conjunction of all the axioms to get a one-axiom aximatization. – Wojowu Oct 21 '18 at 19:50
• shorter means the total number of symbols in the open expansion of all of the axioms. – Zuhair Al-Johar Oct 21 '18 at 20:06
• For this question to make sense you should explain very precisely what language you are using. For instance, I see $\{y \mid \phi(y)\}$, which normally is not part of first-order logic languages. Are you using a first-order language? What is the signature? – Andrej Bauer Oct 21 '18 at 20:47
• @WlodAA No, axiom 2 is about existence of absolute complements and so we must use the bi-conditional. – Zuhair Al-Johar Oct 18 '19 at 22:40
• As a personal opinion:Finding an axiom system (more generally: a description) of a class $K$ of objects which is (at least apparently) essentially different from known axioms/descriptions can express a deep truth about $K$, and can help understand $K$ better. Finding one that is merely shorter seems less helpful/interesting to me. When comparing two axiom systems of humanly readable length for $K$, the shorter one will often be more difficult to understand. (Not always, though; the axiom system {"false"} is very easily understood, but I will not claim that it is equivalent to NF.) – Goldstern Oct 19 '19 at 12:51