I am building upon MO question 102846 concerning the Tarski-Grothendieck set theory (TG).
I have two questions;
1/ I think that it is possible that the axiom of pairing (axiom 4 of the TG theory presented in question 102846) could be deleted. So, my question is: Is axiom 4 independant of the others axioms of the TG set theory ?
2/ In the considered question, it is asserted that the axiom of specification is a consequence of Tarski"s axiom A. My question is: what are the others axioms needed to have this result and could I have a proof ?
Gérard Lang



Tarski-Grothendieck set theory, the axiom of pairing and the axiom of specification
Assume all the axioms of TG except for pairing. We will show that pairing and specification (a.k.a. separation) both follow, with the caveat in the following paragraph.


We will also assume that the empty set exists. This does not seem to follow from the TG axioms as defined in the linked question [What's the difference between ZFC+Grothendieck, ZFC+inaccessible cardinals and Tarski-Grothendieck set theory?](https://mathoverflow.net/questions/102846/) or on Wikipedia <https://en.wikipedia.org/wiki/Tarski-Grothendieck_set_theory>, which do not seem to imply either "there is a set" or "if there is a set then there is an empty set." The natural way to proceed seems to be to postulate the existence of the empty set.


(1) For pairing, suppose we are given sets $x$ and $y$ and we want to form the pair $\lbrace x,y \rbrace$. Let $A$ be a Tarski set containing $x$. Then $A$ also contains some element other than $x$ (this can be seen by considering separately the two cases $x = \emptyset$ and $x \ne \emptyset$.) Define a class function $F$ with domain $A$ by
\begin{equation}
F(z) = \begin{cases}
x & \text{if $z = x$}\newline
y &\text{if $z \in A$ and $z \ne x$}.
\end{cases}
\end{equation}
The range of $F$ is $\lbrace x,y \rbrace$, which is a set by replacement.


(2) For specification, let $A$ be a set and $\varphi$ be a formula. We want to show that the class $B = \lbrace x \in A : \varphi(x)\rbrace$ is a set. If $B$ is empty then we are done because the empty set exists. So we may assume that there is $x\_0 \in A$ such that $\varphi(x\_0)$ holds. Then $B$ is the range of the class function
$F$ with domain $A$ defined by 
\begin{equation}
F(x) = \begin{cases}
x & \text{if $x \in A$ and $\varphi(x)$}\newline
x\_0 &\text{if $x \in A$ and $\neg \varphi(x)$},
\end{cases}
\end{equation}
so it is a set by replacement. 


