Proving in Quine's New Foundations

Question

I'm reading Quine's New Foundations paper. However, there are a lot of questions I do not manage to answer. I would say they all lead to the question: how to prove things in NF? For example, is it provable in NF that

$\forall x (x \in \{x\})$

or commutativity of identity, being this latter defined as

$x = y \stackrel{def}{=} \forall w (x \in w \rightarrow z \in w)$

and finally how do you prove - if possible - that

$x = y \wedge z \in x \rightarrow z \in y$

with just the axioms and definitions Quine provides in his paper?

I came up with these questions in connection with something Quine says in his paper. He says that the "unrestricted" abstraction principle

$\exists x \forall y (y \in x \leftrightarrow \phi)$

for $x$ not occurring in $\phi$, provides a class $x$ about which he says "viz. $\widehat{y} \phi$". Now, I think this means that from the abstraction principle you can prove $\widehat{y}\phi$ for any $\phi$ of the required kind, is it so? I do not even manage to prove that

$x = y \rightarrow x \subset y \wedge y \subset x$

Answer 1

In order to prove in $\mathsf {NF}$ the full set of properties of equality, we need both:

D8. $(a=b) \text { for } (\forall x)((a \in x) \to (b \in x))$,

and extensionality:

P1. $((x \subseteq y) \to ((y \subseteq x) \to (x = y)))$.

From the definition of inclusion:

D7. $(a \subseteq b) \text { for } (\forall x)((x \in a) \to (x \in b))$,

we get: $a \subseteq a$, and applying P1 we get:

1) $a=a$.

From D8, using the abstraction operator (for Quine, using the Principia Mathematica's notation: $\hat x \phi(x)$; in modern terms: $\{ x \mid \phi(x) \}$) , we get:

$(a=b) \to (a \in \{ x \mid \varphi(x) \}) \to (b \in \{ x \mid \varphi(x) \})$

and thus:

2) $(a=b) \to (\varphi(a) \to \varphi(b))$.

Now we can play with $\varphi$ to get:

$(a=b) \to ((a=c) \to (b=c))$,

$((a=b) \land (b=c)) \to (a=c)$,

and:

3) $(a=b) \to (b=a)$.

Now, all the expected rules for equality are in place.

From 2) we get: $(a=b) \to ((a \in c) \to (b \in c))$, as well as: $(a=b) \to ((c \in a) \to (c \in b))$.

Using 3) we conclude with:

$(a=b) \to (\forall x) ((x \in a) \leftrightarrow (x \in b))$.

From extensionality we have:

$((\forall x) ((x \in a) \leftrightarrow (x \in b)) \to (a=b))$,

and thus we finally have:

$(a=b) \leftrightarrow (\forall x) ((x \in a) \leftrightarrow (x \in b))$.

---

Reagarding the singleton we have, by definition of inclusion: $\{ x \} \subseteq a \leftrightarrow (\forall y) (y \in \{ x \} \to y \in a)$, and using the definition of singletion $\{ x \} = \{ z \mid z=x \}$ and the fact that $y \in \{ z \mid z=x \} \leftrightarrow (y=x)$, we get:

$\{ x \} \subseteq a \leftrightarrow (\forall y) (y =x \to y \in a)$.

From equality, we have that: $\phi(x) \leftrightarrow (\forall y)((y = x) \to \phi(y))$, and thus:

$\{ x \} \subseteq a \leftrightarrow (x \in a)$.

But: $\{ x \} \subseteq \{ x \}$, and thus:

$x \in \{ x \}$.