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.

  • 1
    $\begingroup$ "shorter" in what way? Clearly you can take conjunction of all the axioms to get a one-axiom aximatization. $\endgroup$ – Wojowu Oct 21 '18 at 19:50
  • $\begingroup$ shorter means the total number of symbols in the open expansion of all of the axioms. $\endgroup$ – Zuhair Al-Johar Oct 21 '18 at 20:06
  • $\begingroup$ Surely you can cramp them more compactly into one axiom. Two universal axioms $\forall x:\phi(x)$ and $\forall y:\psi(y)$ can be replaced by $\forall x:\phi(x)\wedge\psi(y)$. $\endgroup$ – Wojowu Oct 21 '18 at 20:10
  • $\begingroup$ you mean $\forall x : \phi(x) \wedge \psi(x) $, notice that you are adding the $\wedge$s, but anyhow I'm asking about a really different system from that, and not just a trivial shortening of this system itself $\endgroup$ – Zuhair Al-Johar Oct 21 '18 at 20:13
  • 7
    $\begingroup$ 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? $\endgroup$ – Andrej Bauer Oct 21 '18 at 20:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.