Return to Question

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 $\langle A,B \rangle$ is type-level, then we can define a triplet $ \langle A,B,C \rangle$ using this type-level merit as $\langle \langle A,B \rangle, C \rangle$, 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 a definition of a type-level ordered pair that I've presented to MathStackExchange (see here for details) can indeed be extended to define type-level $\alpha$-tuples, for any ordinal $\alpha$ whether finite or not!

Define: $\iota^2"X = \{ \{\{x\}\}: x \in X\}$

So take any sequence $S: \iota^2"\alpha \to X$, then there exists an $\iota ^2 \alpha$ long tuple $t(S)$ such that:

$$t (S)= \{x \cup \{[\bigcup^2(rng(S))]^*+ i\} | x \in S(\{\{i\}\})\}$$

Where $S(\{\{i\}\})$ is the image of $\{\{i\}\}$ under $S$; and $X^*$ is the smallest ordinal strictly ordinally greater than all elements of $X$

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 \in \alpha$, where each $S(\{\{i\}\})$ is considered as the $i^{th}$ projection of $t(S)$.

To retrieve the $i^{th}$ projection of any such tuple $t(S)$ we define $max^{\alpha}(\bigcup t(S))$ as: $$\{max(d) [ordinal(d) \land d \in x]: x \in \bigcup(t(S))\}$$

Now we retrieve the $i^{th}$ projection of $t(S)$ by taking the set of all elements of $\bigcup(t(S))$ that has the $i^{th}$ ordinal in $max^\alpha(\bigcup(t(S))$ in them, and the $i^{th}$ projection of $t(S)$ would be the image of that set under function $f(X)=X\setminus \{max(d)[ordinal(d) \land d \in X]\}$

My question: Are there comparable examples of type-level infinite tuples in ZFC and its extensions.

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 $\langle A,B \rangle$ is type-level, then we can define a triplet $ \langle A,B,C \rangle$ using this type-level merit as $\langle \langle A,B \rangle, C \rangle$, 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 a definition of a type-level ordered pair that I've presented to MathStackExchange (see here for details) can indeed be extended to define type-level $\alpha$-tuples, for any ordinal $\alpha$ whether finite or not!

Define: $\iota^2"X = \{ \{\{x\}\}: x \in X\}$

So take any sequence $S: \iota^2"\alpha \to X$, then there exists an $\iota ^2 \alpha$ long tuple $t(S)$ such that:

$$t (S)= \{x \cup \{[\bigcup^2(rng(S))]^*+ i\} | x \in S(\{\{i\}\})\}$$

Where $S(\{\{i\}\})$ is the image of $\{\{i\}\}$ under $S$; and $X^*$ is the smallest ordinal strictly ordinally greater than all elements of $X$

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 \in \alpha$. Now we DEFINE the $i^{th}$ projection of $t(S)$ as $S(\{\{i\}\})$; and this way we get a type-level tuple (i.e. of the same type of its projections) of infinite length!

To retrieve the $i^{th}$ projection of any such tuple $t(S)$ we define $max^{\alpha}(\bigcup t(S))$ as: $$\{max(d) [ordinal(d) \land d \in x]: x \in \bigcup(t(S))\}$$

Now we retrieve the $i^{th}$ projection of $t(S)$ by taking the set of all elements of $\bigcup(t(S))$ that has the $i^{th}$ ordinal in $max^\alpha(\bigcup(t(S))$ in them, and the $i^{th}$ projection of $t(S)$ would be the image of that set under function $f(X)=X\setminus \{max(d)[ordinal(d) \land d \in X]\}$

My question: Are there comparable examples of type-level infinite tuples in ZFC and its extensions.

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 $\langle A,B \rangle$ is type-level, then we can define a triplet $ \langle A,B,C \rangle$ using this type-level merit as $\langle \langle A,B \rangle, C \rangle$, 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 a definition of a type-level ordered pair that I've presented to MathStackExchange (see here for details) can indeed be extended to define type-level $\alpha$-tuples, for any ordinal $\alpha$ whether finite or not!

So take any sequence $S: \iota^2"\alpha \to X$, then there exists an $\iota ^2 \alpha$ long tuple $t$ such that:

$$t (S)= \{x \cup \{[\bigcup^2(rng(S))]^*+ i\} | x \in s(\{\{i\}\})\}$$

Where $\iota^2"X = \{ \{\{x\}\}: x \in X\}$

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 \in \alpha$, where each $s(\{\{i\}\})$ is considered as the $i^{th}$ projection of $t(S)$.

To retrieve the $i^{th}$ projection of any such tuple $t(S)$ we define $max^{\alpha}(\bigcup t(S))$ as: $$\{max(d) [ordinal(d) \land d \in x]: x \in \bigcup(t(S))\}$$

Now we retrieve the $i^{th}$ projection of $t(S)$ by taking the set of all elements of $\bigcup(t(S))$ that has the $i^{th}$ ordinal in $max^\alpha(\bigcup(t(S))$ in them, and the $i^{th}$ projection of $t(S)$ would be the image of that set under function $f(X)=X\setminus \{max(d)[ordinal(d) \land d \in X]\}$

My question: Are there comparable examples of type-level infinite tuples in ZFC and its extensions.

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 $\langle A,B \rangle$ is type-level, then we can define a triplet $ \langle A,B,C \rangle$ using this type-level merit as $\langle \langle A,B \rangle, C \rangle$, 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 a definition of a type-level ordered pair that I've presented to MathStackExchange (see here for details) can indeed be extended to define type-level $\alpha$-tuples, for any ordinal $\alpha$ whether finite or not!

Define: $\iota^2"X = \{ \{\{x\}\}: x \in X\}$

So take any sequence $S: \iota^2"\alpha \to X$, then there exists an $\iota ^2 \alpha$ long tuple $t(S)$ such that:

$$t (S)= \{x \cup \{[\bigcup^2(rng(S))]^*+ i\} | x \in S(\{\{i\}\})\}$$

Where $S(\{\{i\}\})$ is the image of $\{\{i\}\}$ under $S$; and $X^*$ is the smallest ordinal strictly ordinally greater than all elements of $X$

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 \in \alpha$, where each $S(\{\{i\}\})$ is considered as the $i^{th}$ projection of $t(S)$.

To retrieve the $i^{th}$ projection of any such tuple $t(S)$ we define $max^{\alpha}(\bigcup t(S))$ as: $$\{max(d) [ordinal(d) \land d \in x]: x \in \bigcup(t(S))\}$$

Now we retrieve the $i^{th}$ projection of $t(S)$ by taking the set of all elements of $\bigcup(t(S))$ that has the $i^{th}$ ordinal in $max^\alpha(\bigcup(t(S))$ in them, and the $i^{th}$ projection of $t(S)$ would be the image of that set under function $f(X)=X\setminus \{max(d)[ordinal(d) \land d \in X]\}$

My question: Are there comparable examples of type-level infinite tuples in ZFC and its extensions.

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 $\langle A,B \rangle$ is type-level, then we can define a triplet $ \langle A,B,C \rangle$ using this type-level merit as $\langle \langle A,B \rangle, C \rangle$, 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 a definition of a type-level ordered pair that I've presented to MathStackExchange (see here for details) can indeed be extended to define type-level $\alpha$-tuples, for any ordinal $\alpha$ whether finite or not!

So take any sequence $S: \alpha \to X$, then there exists an $\alpha$ long tuple $t$ such that:

$$t (S)= \{x \cup \{[\bigcup^2(rng(S))]^*+ i\} | x \in 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 \in \alpha$, where each $s(i)$ is considered as the $i^{th}$ projection of $t(S)$.

To retrieve the $i^{th}$ projection of any such tuple $t(S)$ we define $max^{\alpha}(\bigcup t(S))$ as: $$\{max(d) [ordinal(d) \land d \in x]: x \in \bigcup(t(S))\}$$

Now we retrieve the $i^{th}$ projection of $t(S)$ by taking the set of all elements of $\bigcup(t(S))$ that has the $i^{th}$ ordinal in $max^\alpha(\bigcup(t(S))$ in them, and the $i^{th}$ projection of $t(S)$ would be the image of that set under function $f(X)=X\setminus \{max(d)[ordinal(d) \land d \in X]\}$

My question: Are there comparable examples of type-level infinite tuples in ZFC and its extensions.

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 $\langle A,B \rangle$ is type-level, then we can define a triplet $ \langle A,B,C \rangle$ using this type-level merit as $\langle \langle A,B \rangle, C \rangle$, 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 a definition of a type-level ordered pair that I've presented to MathStackExchange (see here for details) can indeed be extended to define type-level $\alpha$-tuples, for any ordinal $\alpha$ whether finite or not!

So take any sequence $S: \iota^2"\alpha \to X$, then there exists an $\iota ^2 \alpha$ long tuple $t$ such that:

$$t (S)= \{x \cup \{[\bigcup^2(rng(S))]^*+ i\} | x \in s(\{\{i\}\})\}$$

Where $\iota^2"X = \{ \{\{x\}\}: x \in X\}$

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 \in \alpha$, where each $s(\{\{i\}\})$ is considered as the $i^{th}$ projection of $t(S)$.

To retrieve the $i^{th}$ projection of any such tuple $t(S)$ we define $max^{\alpha}(\bigcup t(S))$ as: $$\{max(d) [ordinal(d) \land d \in x]: x \in \bigcup(t(S))\}$$

Now we retrieve the $i^{th}$ projection of $t(S)$ by taking the set of all elements of $\bigcup(t(S))$ that has the $i^{th}$ ordinal in $max^\alpha(\bigcup(t(S))$ in them, and the $i^{th}$ projection of $t(S)$ would be the image of that set under function $f(X)=X\setminus \{max(d)[ordinal(d) \land d \in X]\}$

My question: Are there comparable examples of type-level infinite tuples in ZFC and its extensions.