Ordered Pairs

A one type higher level ordered pairs, it requires full Extensionality.

(A,B)={y|y=(AU{1})\{2}Vy=(BU{2})\{1}V(y=m^~1eA)V(y=n^2eA)V(y=o^~2eB)V(y=k^1eB)} 

where m,n,o,k all do not contain 1 nor 2 as elements of. 

Of course 1,2,m,n,o,k are all constants. 

The definition of projections is clear: 

A is 1st of p <-> Exep (1ex^Ay(yeA<->(yex^(mep->~y=1))V(nep^y=2))) 

B is 2nd of p <-> Exep (2ex^Ay(yeB<->(yex^(oep->~y=2))V(kep^y=1))) 

No need for axiom of infinity at all. 

A simpler pair along the same lines would be: 

(A,B) = {y| 

[y=A\{0} or y=BU{0} or (0 e A ^ y=0) or (~0 e B ^ y={0})] ^ 

[A=0 -> y=/=0] ^ 

[B={0} -> y=/={0}]} 

This has a shorter defining formula than Holmes pair and the one above. Even definition of projections is shorter 

x is 1st of p <-> x={y| Exist z e p (~0 e z ^ y e z)  or (0 e p ^ y=0)} 

x is 2nd of p <-> x={y| (y=0 or Exist z e p (0 e z ^ y e z)) ^ ({0} e p -> ~y=0)} 

Of course all of the above is written in fully stratified language. Writing it in LaTex:

$\langle A,B \rangle = \{A \setminus \{0\} \} \setminus  \{A \cap\{0\}\} \cup \\\{B \cup \{0\}\} \setminus \{B \cap\{0\}\}\cup \\ \{A' \cap \{0\}\} \setminus \{\{0\}\}\cup \\ \{B' \cap \{0\}\} \cap \{\{0\}\}$

$First(p)=\{x| \exists q \in p (0 \not \in q \land x \in q) \lor (0 \in p \land x=0) \}$

$Second(p)=\{x| (x=0 \lor \exists q \in p (0 \in q \land x \in q)) \land (x=0 \to \{\{0\}\} \not \in p)\}$

That is:

⟨A,B⟩={A∖{0}}∖{A∩{0}}∪

{B∪{0}}∖{B∩{0}}∪

{A′∩{0}}∖{{0}}∪

{B′∩{0}}∩{{0}}

1st(p)={x|∃q∈p(0∉q∧x∈q)∨(0∈p∧x=0)}

2nd(p)={x|(x=0∨∃q∈p(0∈q∧x∈q)) ∧(x=0→{{0}}∉p)}

Cartesian products with colored ordered pairs

The use of ordered pairs in relations can be dispensed with altogether by the use of unordered pairs + colouring. 

The informal idea of colouring is that if I have a set A and a set B then we'd pick a colour C such that no member of A nor of B has that colour and then colour all members of B with C, and then take the set of all unordered pairs {a,b_C} where a is an element of A and b_C is an element of B coloured with C, this set would serve as a Cartesian product of A and B, however this Cartesian product would be relativized to C, so it is C_AxB really. 

To capture that formally we take any set C that is not an element of any element of A and that is not an element of any element of B, and then we take the set B_C={xU{C}| x in B}, i.e. B_C is the set of all unions of elements of B with {C}. Now the C_Cartesian product of A and B would be defined as: 

C_AxB = {{a,b}| a in A & b in B_C} 

In well founded set theories we can get rid of C altogether, since we do have a uniform way of producing a unique set that is not an element of elements of A and B, for each A,B. This is simply the set {A,B}! and then we proceed with colouring in the above manner, so the Cartesian product of A and B would be defined as: 

AxB = {{a,bU{{A,B}}}| a in A & b in B} 

The idea is by colouring of elements of B the sets A and the coloured B (which is {bU{{A,B}}| b in B}, would be DISJOINT sets, and for any disjoint sets X,Y the set of all unordered pairs of elements of them do serve as the Cartesian product of them, i.e. there is no need for using a general concept of ordered pairs for this case. 

Zuhair 

1. Modified Holmes's triplet:

$\langle X,Y,Z \rangle  = \{\{x\},\{y,0,1\},\{y,2,3\}, \{z,4,5\},\{z,6,7\}| x \in X, y \in Y, z \in Z\}$

$first(p)= \{x | \{x\} \in p\}$

$second(p)= \{y | \{y,0,1\},\{y,2,3\} \in p\}$

$third(p)  =   \{z  | \{z,4,5\},\{z,6,7\} \in p\}$

2. My triplets:

⟨X,Y,Z⟩={{x,1},{y,2},{z,3},{4,5}∪(X∩{2,3}),

{4,6}∪ (Y∩{1,3}),{4,7}∪(Z∩{1,2})|x∈X,y∈Y,z∈Z}

First(p)={x|{x,1}∈p∧(x∈{2,3}→∃k({4,5,x,k}∈p)}

Second(p)={y|{y,2}∈p∧(y∈{1,3}→∃k({4,6,y,k}∈p)}

Third(p)={z|{z,3}∈p∧(z∈{1,2}→∃k({4,7,z,k}∈p)}

Written full in LaTeX:

$\langle X,Y,Z \rangle = \{\{x,1\},\{y,2\},\{z,3\},\\ \{4,5\} \cup (X \cap \{2,3\}), \{4,6\} \cup (Y \cap \{1,3\}), \\\{4,7\} \cup (Z \cap \{1,2\}) | x \in X, y \in Y, z \in Z\}$ 

$First(p) = \{x|\{x,1\} \in p \land (x \in \{2,3\} \to \exists k(\{4,5,x,k\}\in p))\}$

$Second(p)=\{y|\{y,2\} \in p \land (y \in \{1,3\} \to \exists k(\{4,6,y,k\}\in p))\}$

$Third(p)=\{z|\{z,3\} \in p \land (z \in \{1,2\} \to \exists k(\{4,7,z,k\}\in p)) \}$

Holmes's pairs has simpler definition, mine has simpler structure in terms of cardinality of most of its members and of the triplet itself.

A type level ordered pair other than Quine-Rosser's:

The following is a definition of a new type-level ordered pair:

⟨A,B⟩={x∪{(⋃(A∪B))∗},y∪{(⋃(A∪B))∗+1}|x∈A,y∈B}

where: X∗=min(α)[∀x∈X(ordinal(x)→x<α)]

In English: X∗X∗ is the minimal ordinal strictly larger than all ordinals in XX.

Where: x=min(y)[ϕ(y)]≡dfϕ(x)∧∀y(ϕ(y)→x≤y)

Now to retrieve back the first and second projections of this pair, its very easy, we first define max2(X) as the maximal two ordinals in X. Now take any pair p, take max2(⋃(p)), then apply separation on p and take all elements of p that have the minimal element of max2(⋃(p)) as an element of, this set would be A+ and then strip away the maximal ordinal in elements A+ from those elements using separation on P(⋃(A+)) and we get the first projection of p, that is A. Similarly 

we retrieve the second projection B 

 of p by applying the same argument but by using the maximal element of max2(⋃(p)).

This pair can be used in ZFC, but not in NF related systems nor in NBG\MK over classes, since those can have big sets or classes that contain all set ordinals. So this fall short of the Quine-Rosser type-level ordered pair which work in all of the above-mentioned theories. However its equivalent to it over ZF and its extensions.

Of course we can get new definitions of type level ordered pairs by replacing the conditions ‘‘ordinal,<"‘‘ordinal,<" in the above definition by any predicates P,R as far as P defines a proper class that is well ordered by R, so every set in the theory would have an R-limit on elements of it that satisfy P, that is outside it of course.1

Quine-Rosser ordered pair is type-level; i.e., it is definable by a stratified formula that assigns to it the same type it assigns to its projections.

It is known that if ⟨A,B⟩ is type-level, then we can define a triplet ⟨A,B,C⟩using this type-level merit as ⟨⟨A,B⟩,C⟩, , and we can go up recursively to define any n-tuple.

However, this extend-ability seems to fail to define infinite type-level tuples, since functions of Quine-Rosser pairs are one type higher than the pairs in them.

Now the definition above can be extended to define type-level α-tuples, for any ordinal α whether finite or not!

So take any sequence S:α→X, then there exists an α long tuple t(S) such that:

t(S)={x∪{[⋃2(rng(S))]∗+i}|x∈s(i)}

Now clearly t(S)is of the same type of elements of the range of S, i.e. t(S) has the same type of each s(i)where i∈α, where each s(i) is considered as the ith projection of t(S).

To retrieve the ith projection of any such tuple t(S) we define maxα(⋃t(S)) as:

{max(d)[ordinal(d)∧d∈x]:x∈⋃(t(S))}

Now we retrieve the ithprojection of t(S)by taking the set of all elements of ⋃(t(S))that has the ithordinal in maxα(⋃(t(S)) in them, and the ithprojection of t(S)would be the image of that set under function

 

f(X)=X∖{max(d)[ordinal(d)∧d∈X]}Modified Quine-Rosser tuples:

These are stronger tuples, in the sense that they work under weaker assumptions.

Statement: for any ordinal \alpha, there is a tuple of length T^2 \alpha, and there will be no limitation on which sets can be a projection of it.

Let D be the set of all Ordinals. 

Define functions $F_i$ for $i \in D\{0}$ as: 

$F_i(X)= [X \setminus D] \cup \{d+*(i+*1)| d \in D \cap X \} \cup \{i\} $

Now the tuple $t^alpha(S)$ whose projections are entries s_i of the sequence S from \itoa^2" \alpha \to  V, is defined as: 

$ t^alpha(S) = \{F_i(x)| x \in s_\{\{i\}\} \in rng(S) \land  \{\{i\}\} \in \iota^2" \alpha \}$

and were "+*" is "Hessenberg natural sum", defined as:

where "max" mean "ordinal greater than". 

Now to retrieve back the i_th projection from the pair, the smallest ordinal member of the elements of the pair would serve as the indicator of the projection, so take the set of all elements of the tuple having ordinal i as the smallest ordinal in them, and taking the converse function F^-1 over those would yield the i^{th} projection of the tuple. 

So the definition of the i^{th} projection of p is simply:

i^{th} (p) = \{ x | F_i(x) \in p \}

So this mean that this tuple work in the most general manner that a tuple can work in NF\NFU, and of course in ZFC, NBG, MK set theories. 

Randall Holmes version of modified Q-R tuples:

Define inc as the function sending (x,n) to (x,n+1) for any x and any natural number n, and fixing anything not in V x N

Now define A_x as the {inc``B \cup {(x,0)}: B E A}  This "increments" all elements of elements of A which are in V x N and adds (x,0) as a further element of each element.

For any function f with domain the set of all double singletons, define tuple(f) as the union of all (f({{x}})_x

This gives a T^2(|V|) tuple with projections at the same type as the tuple.

I think that the limit on how many projections there are is intrinsic.

A closely related observation of mine is that we can use similar method to have type level functions of maximally T|V| many entries!

 For every function f whose domain is a set of singletons, there is a type-level function t(f) corresponding to it defined as:

t(f)={(x,z)|z∈f({x})}

Where (,) is the Quine-Rosser type-level pair

Possibly the longest tuples ever are present at:

Mathoverflow

 

IMPLEMENTING RELATIONS AS CONFLUENCE OF ORDERED PAIRS.

Define a binary function P in the language of set theory that obeys the characteristic property of ordered pairs and such that for any two sets A,B, for any definable relation R, there exists a set R∗ such that:

Notice that ⋃(R∗) would be able to represent a relation even though it is NOT a set of ordered pairs!

Using the language of type theory this way we can have a relation of type n being composed (i.e. is the union of) of type n ordered pairs!

R∗={P(a,b)|a∈A∧b∈B∧a R b}∧∀a∈A ∀b∈B[∃X(X⊆⋃(R∗)∧X=P(a,b))↔a R b] ?