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
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
12
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.
-
$\begingroup$ Dear Trevor, I have the following question with your proof (1). It seems that you need the pairing concept o build the function concept. So, if you are using a function to prove the pairing axiom, how to be sure that we are not having a vicious circle ? Gérard Lang $\endgroup$ Aug 12, 2012 at 6:28
-
$\begingroup$ Dear Gérard, that is a good question. I'm using the term "class function" to refer to the defining formula of F together with parameters in the definition ($x$ and $y$.) So it's not a priori an object in the domain of discourse, it's just shorthand for a syntactical notion. This may be an abuse of notation but it's common in set theory. To translate what I wrote into a formal proof, one uses the instance of the replacement schema corresponding to the formula that defines F as a binary relation. $\endgroup$ Aug 12, 2012 at 15:15
-
$\begingroup$ I should add that it's important that we consider $F$ as a binary relation, not as a unary relation on ordered pairs, or else your objection would apply. In the (ostensible) absence of the pairing axiom the difference becomes rather confusing and one has to look at the formal statement of the replacement axiom schema to understand what is going on. $\endgroup$ Aug 12, 2012 at 15:51
-
$\begingroup$ E.g., for (1) we are using the instance of the replacement axiom schema corresponding to the formula $\varphi$ with parameters $x$, $y$, and $A$ given by $\varphi(z,t) \iff z = t = x \text{ or } (z \in A \text{ and } z \ne x \text{ and } t = y)$. $\endgroup$ Aug 12, 2012 at 16:23
-
$\begingroup$ Dear Trevor, thank you for your precisions. here are some comments. A/Concerning my question 2, your proof is the classical derivation of the separation schema from the replacement schema.I was hoping, in the context of the assertion of question Mo 10284O that the axiom of specification/separation is a consequence of axiom A of Tarski, to have a proof of the separation axiom from axiom A without replacement. More precisely, I was hoping to have a derivation of the schema of separation from the TG set theory minus Replacement. B/Concerning question 1, I fear I am not completely convinced. $\endgroup$ Aug 12, 2012 at 18:19