Tarski-Grothendieck set theory, the axiom of pairing and the axiom of specification 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
 A: 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? 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. 
