# What's the proof of inconsistency of this theory?

Let $$T$$ be a first order theory, whose axioms are Extensionality, Pairing, and all instances of Class Comprehension schema (outlined below).

Define: $$set(x) \equiv_{df} \exists y (x \in y)$$

1. Extensionality: $$\forall z ( z \in x \leftrightarrow z \in y ) \to x=y$$

2. Class Comprehension: if $$\phi$$ is a formula in which $$x$$ never occur, then all closures of: $$\exists x \forall y (y \in x \leftrightarrow set(y) \land \phi)$$; are axioms.

Define: $$x=\{y|\phi\} \equiv_{df} \forall y (y \in x \leftrightarrow set(y) \land \phi)$$

Define: $$x=V \equiv_{df} \forall y (set(y) \to y \in x)$$

3. Pairing: $$\forall \text{ sets } a,b \exists \text{ set } x \forall y (y \in x \leftrightarrow y=a \lor y=b)$$

I think it must be inconsistent to add the following axiom schema on top of $$T$$

If $$\phi$$ is a formula in which only symbol $$y$$ occur free, and only free, then

$$(T \not \vdash \{y| \phi\} \not \in V) \to \{y|\phi\} \in V$$; is an axiom.

What is the proof of that inconsistency?

• @MaliceVidrine, the assertion is a limited one and it is negative, so how can you get the positive form? Jan 23, 2020 at 12:53
• Ah, yes; then I have a follow-up question: do you mean to phrase pairing that way, or do you mean to restrict pairing to sets? Jan 23, 2020 at 17:38
• @MaliceVidrine, thanks for the correction on pairing. I meant the pair of sets is a set. I've corrected it. Jan 23, 2020 at 18:07

Let $$\theta$$ be a sentence independent of $$T$$ (which exists since $$T$$ is a subtheory of NBG, say) and consider the formulas $$\varphi(y)\equiv \theta\wedge(y\not\in y),\quad\psi(y)\equiv\neg\theta\wedge(y\not\in y).$$ Both $$\{y:\varphi\}\in V$$ and $$\{y:\psi\}\in V$$ are consistent with $$T$$ since by choice of $$\theta$$ we can find models of $$T$$ in which one or the other is $$\emptyset$$. So in any model of your theory, we must have $$\{y: y\not\in y\}\in V$$ (apply the final scheme to $$\varphi$$ or $$\psi$$ depending on whether $$\theta$$ holds in this model). That is, the Russell class must be a set in any model of your theory - which is impossible.
• The real issue is how does this theory relate to the consistency of other theories. For example if we say that Zermelo set theory is consistent, then this would imply infinity in this theory, and actually prove all sets in $V_\omega$ to be sets here, since if not then this would mean that Zermelo is inconsistent!? Not only that! It would prove the existence of a model of Zermelo also! The point is that you cannot prove the consistency of this system in any extension of ZF? Since it would prove a model of the latter. Perhaps I'm baffled, but that's how matters appears to me? Jan 23, 2020 at 18:57
• @Zuhair Wait, I may have misinterpreted your notation: in "$\{y:\varphi\}$," does $y$ range over sets (in which case $V_{\omega+1}$ satisfies your theory trivially) or classes (in which case things are more interesting)? Jan 23, 2020 at 19:03
• Oh, No. I should say that my original intention is for $y$ in $\{y|\phi\}$ to range over sets of course. But the term $\{y|\phi\}$ to range over classes. That's what I meant by "of course", I misread your comment, I thought you were asking about $\{y|\phi\}$ and not about the $y$ in it. Anyhow it is interesting to see if there is an interesting alternative as you've mentioned, but I must be honest here, that was not my question. Sorry for the misunderstanding. Jan 23, 2020 at 19:36
• @Zuhair Please unaccept my answer until you've read the edit I just made - I was incorrect, since I misread your scheme (the "$\in V$" specifically). In particular, as you said $V_{\omega+1}$ is not a model of your theory, since it's consistent with $T$ that $HF\in Sets$ (as $V_{\omega\cdot 2+1}\models T$) but in $V_{\omega+1}$ we have $Sets=V_\omega=HF\not\in V_\omega$. Jan 23, 2020 at 21:38