Existence of Middle Universal Product
Theorem
For each $m \in \N$, the following is a theorem of von Neumann-Bernays-Gödel set theory:
- $\forall X: \exists Z: \forall v_1, \dotsc, v_m: \forall x, y: \sequence {x, v_1, \dotsc, v_m, y} \in Z \iff \tuple {x, y} \in X$
where the notation $\sequence {\cdot, \dotsc, \cdot}$ is defined inductively as:
- $\sequence {y_1} := y_1$
- $\sequence {y_1, \dotsc, y_k, y_{k + 1}} := \tuple {\sequence {y_1, \dotsc, y_k}, y_{k + 1}}$
and $\tuple {\cdot, \cdot}$ denotes the Kuratowski formalization of ordered pairs.
Corollary
For each $n \in \N_{> 0}$ and $m \in \N$, the following is a theorem of von Neumann-Bernays-Gödel set theory:
- $\forall X: \exists Z: \forall v_1, \dotsc, v_m: \forall x_1, \dotsc, x_n: \forall y: \sequence {x_1, \dotsc, x_n, v_1, \dotsc, v_m, y} \in Z \iff \sequence {x_1, \dotsc, x_n, y} \in X$
Proof
In the metatheory in which NBG is formalized, we proceed by induction on $m$.
Basis for the Induction
If $m = 0$, the theorem is:
- $\forall X: \exists Z: \forall x, y: \sequence {x, y} \in Z \iff \tuple {x, y} \in X$
But, by unfolding the definition of $\sequence {x, y}$, we observe that it is precisely $\tuple {x, y}$.
Therefore, $Z := X$ satisfies the basis for the induction.
$\Box$
Induction Hypothesis
As the induction hypothesis, assume that:
- $\forall X: \exists Z: \forall v_1, \dotsc, v_m: \forall x, y: \sequence {x, v_1, \dotsc, v_m, y} \in Z \iff \tuple {x, y} \in X$
for some arbitrary $m \in \N$
From this, we will prove:
- $\forall X: \exists Z: \forall v_1, \dotsc, v_m, v_{m + 1}: \forall x, y: \sequence {x, v_1, \dotsc, v_m, v_{m + 1}, y} \in Z \iff \tuple {x, y} \in X$
Induction Step
Let $X$ be arbitrary.
Apply the induction hypothesis to find a class $Z$ such that:
- $\forall v_1, \dotsc, v_m: \forall x, y: \sequence {x, v_1, \dotsc, v_m, y} \in Z \iff \tuple {x, y} \in X$
Next we will use the following:
Lemma
The following is a theorem of von Neumann-Bernays-Gödel set theory:
- $\forall X: \exists Z: \forall u, v, w: \tuple {\tuple {u, v}, w} \in Z \iff \tuple {u, w} \in X$
$\Box$
Applying the lemma to $Z$, there is a class $Z'$ such that:
- $\forall u, v, w: \tuple {\tuple {u, v}, w} \in Z' \iff \tuple {u, w} \in Z$
In particular, for $u = \sequence {x, v_1, \dotsc, v_m}$, $v = v_{m + 1}$, and $w = y$:
- $\forall v_1, \dotsc, v_m: \forall x, y: \tuple {\tuple {\sequence {x, v_1, \dotsc, v_m}, v_{m + 1}}, y} \in Z' \iff \tuple {\sequence {x, v_1, \dotsc, v_m}, y} \in Z$
But by definition of the notation $\sequence {\cdot, \dotsc, \cdot}$, that is equivalent to:
- $\forall v_1, \dotsc, v_m: \forall x, y: \sequence {x, v_1, \dotsc, v_m, v_{m + 1}, y} \in Z' \iff \sequence {x, v_1, \dotsc, v_m, y} \in Z$
Finally, by Biconditional is Transitive with the definition of $Z$:
- $\forall v_1, \dotsc, v_m: \forall x, y: \sequence {x, v_1, \dotsc, v_m, v_{m + 1}, y} \in Z' \iff \tuple {x, y} \in X$
Therefore, $Z'$ satisfies the induction step.
$\Box$
By the Principle of Mathematical Induction, the theorem follows.
$\blacksquare$