I'm studying the one-sorted version of NBG (Neumann-Bernays-Gödel) Class Theory (that is, NBG with only one alphabet). I want to prove that $\vdash \exists z(\exists Z(z\in Z)\wedge z=\{x,y\})$ but I don't how.
Below are some inference rules and axioms I'm using:
Axiom: Let $\Gamma$ be a list of formulas, $\phi ,\psi$ be two formulas e $x,y$ be two variables. We assume that
- $\forall x\phi \vdash \phi $. Moreover, if $y$ is not a bounded variable of $\phi$, then $\forall x\phi \vdash \phi [y/x]$
- Suppose that $x$ isn't a free variable of $\psi$. If $\Gamma,\phi \vdash \psi$, then $\Gamma,\exists x\phi \vdash \psi $.
I want to emphasize that I'm NOT using the existential instantiation.
Let $\phi$ be a formula. We denote
- $\color{red}{\forall \overline{x}(\phi (\overline{x}))}:=\forall x\big(\exists X(x\in X)\Rightarrow \phi (x)\big)$
- $\color{red}{\exists {\overline x}(\phi (\overline{x}))}:=\exists x\big(\exists X(x\in X)\wedge \phi (x)\big)$.
Axiom of Pairing: We assume that
$$\vdash \forall \overline{x}\forall \overline{y}\exists \overline{z}\forall w\big(w\in \overline{z}\Leftrightarrow (w=\overline{x}\vee w=\overline{y})\big)$$
Below is what I did:
Definition: Let $x,y,Z$ be three classes. We say that $x$ and $y$ are the only elements of $Z$ if $\vdash \forall w\big(w\in Z\Leftrightarrow (w=x\vee w=y)\big)$
Proposition: Let $x,y,Z_1,Z_2$ be four classes. If $x$ and $y$ are the only elements of $Z_1$, then $(Z_2=Z_1)\equiv \forall w\big(w\in Z_2\Leftrightarrow (w=x\vee w=y)\big)$.
Because of the previous proposition, if $x$ and $y$ are the only elements of a class $Z$, then we can denote $Z$ by $\color{red}{\{x,y\}}$.
Using the axiom of pairing and the previous notations, I want to prove that, given any two sets $x$ and $y$, we have $\vdash \exists \overline{z}(\overline{z}=\{x,y\})$. That is, I want to prove that if $\vdash \exists X(x\in X)$ and $\vdash \exists Y(y\in Y)$ then $\vdash \exists z\big(\exists Z(z\in Z)\wedge z=\{x,y\}\big)$.
I was able to prove that
$$\vdash \exists z\big(\exists Z(z\in Z)\wedge \forall w(w\in z\Leftrightarrow (w=x\vee w=y))\big)\color{red}{(1)}.$$
So, to prove what I want, I just need to prove that $\vdash \forall w\big(w\in z\Leftrightarrow (w=x\vee w=y)\big)$ and use the previous proposition. However, since existential instantiation isn't allowed, I don't know how to obtain the previous deduction from $(1)$ and from the basic rules of inference.
Thank you for your attention!