1
$\begingroup$

Working in $\sf ZFA$, or in $\sf NFU$:

We split the universe $V$ into two disjoint subclasses $\mathcal V_1, \mathcal V_2$ that are equinumerous with $V$

Now we take two bijections:

$F_1: V \to P^+(\mathcal V_1) \\ F_2: V \to P^+(\mathcal V_2)$

, where: $P^+(X)=\{y \subseteq X \mid y \in V \land \exists z : z \in y \}$

Now we define a type-level ordered pair, simply as: $$(a,b) = F_1(a) \cup F_2(b)$$

Retrieving projections is easy, to get the first projection simply intersect $(a,b)$ with $\mathcal V_1$, then apply $F_1^{-1}$; to get the second projection simply intersect $(a,b)$ with $\mathcal V_2$, then apply $F_2^{-1}$. In nutshell:

Define: $\operatorname {Pair}(p) \iff \exists a \exists b: p=F_1(a) \cup F_2(b) $

$ \begin{align} \operatorname {Pair}(p) \to & \pi_1 (p) = F_1^{-1}(p \cap \mathcal V_1) \ \land \\ &\pi_2 (p) = F_2^{-1} (p \cap \mathcal V_2)\end{align}$

Extending this pair to an $\lambda$-tuple is immediate: $$(x_1,x_2,..)_\lambda = \bigcup_{\alpha<\lambda} F_\alpha (x_\alpha)$$

with Projections given by: $$\pi_\alpha (p) = F^{-1}_\alpha(p \cap \mathcal V_\alpha )$$

To extend it to proper classes, we need to upgrade the $F_\alpha$ bijections to:

$ F_\alpha: \mathcal P(V) \to \mathcal P^+(\mathcal V_\alpha)$

Where $\mathcal P^+(X)$ is the class of all nonempty subclasses of $X$.

This is a simple general way of having type-level ordered pairs\tuples, it works under lack of Extensionality, unlike Quine-Rosser type-level pairs which suffocate by existence of any Ur-element (atom).

However, this pair\tuple does require that $|A| \leq |P^+(V)|$; where $A$ is the class of all Atoms, which is there in $\sf ZFA$, but not fulfilled by any of the known models of $\sf NFU$. If $\sf NF$ proves to be consistent, then this would be equivalent to having as many Atoms as Sets, and so having those pairs would interpret $\sf NF$.

It appears to me that this is so simple that it must have been pondered before, hence my question is about reference to this particular way of defining ordered pairs\tuples.

Had those tuples been worked up before? References?

$\endgroup$

0

You must log in to answer this question.

Browse other questions tagged .