===== Set theory =====
==== Framework ====
This wiki is a place where I can look up definitions of mathematical objects and also see their generalizations and special cases. Set theory is the most commonly chosen way to set up mathematical foundations, and accordingly most of the entries in the wiki specify mathematical sets.
=== Axiom systems ===
This entry is not about choosing any specific axiomatic system, but just to list what's out there. Below I present some of the standard axioms for set theory. The strength of the total system of axioms is that of [[http://en.wikipedia.org/wiki/Tarski-Grothendieck_set_theory|Tarski Grothendieck set theory]]. I elaborate on the notion of //strength of a set theory// in the Discussion section below. Most of the concepts presented on //axiomsofchoice.org// can be reasoned about //within// this theory. 

=== Notation I ===

Firstly, some notational conventions for the remaining article. Let latin latters be be variables in the domain of discourse, 

^ $x,y,z,u,X,Y,Z,s,p,U,\dots$ ^

possibly indexed,

^ $z_1,z_2,z_3,\dots$ ^

and let the greek letters be predicate symbols

^ $\phi,\psi,\dots$ ^

Set theory, as given in a standard presentation like below, is a theory in predicate logic whos signature involves a single binary predicate "$\in$". This symbol is given meaning in the axioms that follow, which thereby //implicitly// define the notion of //set//. To state the axioms concisely, we now introduce some convenient notation. From a first order logic point of view, this can be considered and extension of the theories vocabulary.

First, we use

| @#EEEE55: predicate   | @#EEEE55: $ x \notin X \equiv \neg (x \in X) $ |

Next we effectively introduce a restricted quantification "over the set $X$", which is analog to the [[http://en.wikipedia.org/wiki/Bounded_quantifier|Bounded quantifier]] in arithmetic. Note, however, that this is only the interpretation: From the formal point of view, we always quantify over the whole domain of discourse and there is no new quantifier (or "set" containing something, for that matter) and we merely use these symbols in rewriting certain predicates.  

| @#EEEE55: predicate   | @#EEEE55: $\forall (x\in X).\ \phi(x) \equiv \forall x.\ (x\in X \Rightarrow \phi(x)) $ |
| @#EEEE55: predicate   | @#EEEE55: $ \exists (x\in X).\ \phi(x) \equiv \exists x.\ (x\in X \land \phi(x)) $ |

Now we introduce a 2-ary predicate "$\subseteq$" expressing the subset property and also some predicates which built on it. One could says that it is as important as the predicate $\in$ itself. 

| @#EEEE55: predicate   | @#EEEE55: $ X\subseteq Y \equiv \forall (x\in X).\ (x\in Y) $ |
| @#EEEE55: predicate   | @#EEEE55: $ X\subset Y \equiv X\subseteq Y \land X\neq Y $ |

We also write 

| @#EEEE55: predicate   | @#EEEE55: $ X\subset Y \equiv X \subsetneq Y \equiv Y \supset X \equiv Y \supsetneq X $ |

Warning: In the literature, $ X\subset Y $ is often used to denote $ X\subseteq Y $ as well.

One simple predicate that builds on $\subseteq$ is transitivity:

| @#EEEE55: predicate   | @#EEEE55: $X$...transitive $\equiv \forall (Y\in X).\ Y\subseteq X$ |

The following predicate expresses equinumerosity, and we state it because it's part of the Tarski Axiom: Two sets $X$ and $Y$ are "equally big" if there is a set $Z$ which puts all the elements of $X$ and $Y$ in one-to-one correspondence via ordered pairs. 

| @#EEEE55: predicate   | @#EEEE55: $ X\approx_{eq} Y \equiv \exists Z.\ [ (\forall(x\in X).\ \exists(y\in Y).\ \langle x,y \rangle \in Z) \land (\forall(y\in Y).\ \exists(x\in X).\ \langle x,y \rangle \in Z) \land (\forall x,y,z,u.\ [\langle x,y \rangle \in Z \land \langle z,u \rangle \in Z] \Rightarrow [x=z \Leftrightarrow y=u])] $ |

>Here I already use the [[ordered pair]] which I formally denfine only at a later point - this can be avoided by writing it down using primitive logical symbols (see [[http://us.metamath.org/mpeuni/grothprim.html|grothprim]] and also [[Grothendieck universe]]), and maybe I should, but then one deals with an even longer expression.

=== Some standard axioms ===
== "Equality axiom" ==

The first axiom presented is very standard. The condition for equality of sets is defined in terms of the predicate "$\in$".  [[http://en.wikipedia.org/wiki/Axiom_of_extensionality|Axiom of Extensionality]]: If any two sets $x,y$ have the same elements, then $x$ and $y$ are equal. Notice that the converse is already true from logic: If for two terms $x,y$ holds $x=y$, then any predicate statement such as $z\in x$ is equal to $z\in y$.

^ $ \forall x,y.\ [ \forall z.\ (z \in x \Leftrightarrow z \in y) \Rightarrow x = y] $ ^

== "Non-existence axiom" ==

The following axiom is related to foundational problems of set theory. [[http://en.wikipedia.org/wiki/Axiom_of_regularity|Axiom of Regularity]]. In a sense, the second axiom excludes certain constructions from being sets, which in princple could be captured by the logical language: Given a nonempty set $X$, it must contain an element which itself doesn't contain another element of $X$. The non-existence of self-including sets follows for example from considering such a set and applying the axiom to the singleton containing it. 

^ $ \forall X.\,\left[\exists z.\,(z\in X)\right] \Rightarrow \left[\exists (y\in X).\,\nexists (z\in X).\,(z \in y)\right] $ ^

== "Existence axioms" ==

The remaining axioms grant //existence// of sets with certain properties. 

Firstly, we want to guarantee that the theory is non-empty so there actually does exist at least //any// set. Formally, we postulate that there exists a set $x$ such that a certain dummy proposition about it holds and that proposition is chosen to be a tautology with respect to the underlying logic. More concretely, we let the existential quantification $\exists x$ be followed by the "$x=x$", which is true by reflexivity of "$=$". Related to the following axiom is the [[http://en.wikipedia.org/wiki/Axiom_of_empty_set|Axiom of empty set]], which some set theories use. We, however, conclude the existence of the emptry set from Axiom of Replacement stated further below. 

^ $ \exists x.\ (x=x) $ ^

For any two sets, we state the existence of the [[unordered pair]], the set containing these two sets. The unordered pair then is unique by extensionality. The [[singleton]] follows then from the pair of two equal elements. 
[[http://en.wikipedia.org/wiki/Axiom_of_pairing|Axiom of Pairing]]: For any two given sets $x,y$, there is another set $Z$ containing exactly $x$ and $y$. 

^ $ \forall x, y.\ \exists Z.\ \forall z.\ [ (z \in Z) \Leftrightarrow (z = x \lor z = y)] $ ^

[[http://en.wikipedia.org/wiki/Axiom_of_union|Axiom of Union]]: For any set $X$ there is a set $u$, which contains the elements of all of $X$'s elements. 

^ $ \forall X.\ \exists u.\ \forall z.\ [(z \in u) \Leftrightarrow \exists(x\in X).\ (z \in x)] $ ^

There are various formulations of the next postulate in set theory, which vary in strength. The following postulate is not a single axiom but an [[http://en.wikipedia.org/wiki/Axiom_schema|axioms schema]], providing an axiom for all suitable logical formulas $\phi$. [[https://en.wikipedia.org/wiki/Axiom_schema_of_replacement|Axiom schema of Replacement]]: Given a logical formula which let's you specify sets $y$ by certain other sets $x\in X$, then there exists the set $Y$, which contain these $y$. Each $y$ must be uniquely singled out w.r.t. the elements of the "indexing" set $X$ and, of course, the formula can't already assume the existence of $Y$. The meaning of the axiom schema is sometimes paraphrased as: The range $Y$ of a "function" with domain $X$ is a set itself. 

^ $ \forall z_1,\dots, z_n, X.\ ( [ \forall (x\in X).\ \exists_! y. \ \phi(x, y, z_1, \dots, z_n, X) ] \Rightarrow \exists Y. \ \forall y. \ [(y \in Y) \Leftrightarrow \exists (x\in X).\ \phi(x, y, z_1, \dots, z_n, X) ] ) $ ^

== "Beyond ZFC" ==

Lastly we postulate an axiom, not included in [[http://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory|ZFC]], the [[http://en.wikipedia.org/wiki/Tarski-Grothendieck_set_theory|Tarski Axiom]]: Given a set $x$, there exists a Grothendieck universe $U$ containing $x$ it, see the discussion section. 

^ $ \forall x.\ \exists U.\ ((x \in U) \land \forall (y\in U).\ [\forall s.\ (s \subseteq y \Rightarrow s \in U) \land \exists (p\in U).\ \forall s.\ (s \subseteq y \Rightarrow s \in p)] \land \forall S.\ [(S \subseteq U) \Rightarrow (S \approx_{eq} U \lor S \in U)]) $ ^

Breaking down the Tarski Axiom:
| @#DDDDDD: range       | @#DDDDDD: $ \forall x.\ \exists U.\ $ | @#DDDDDD: range       | @#DDDDDD: For all sets $x$, there is a set $U$ |
| @#DDDDDD: range       | @#DDDDDD: $ x \in U $ | @#DDDDDD: range       | @#DDDDDD: such that $x$ itself is in $U$, |
| @#DDDDDD: range       | @#DDDDDD: $ \forall (y\in U).\ \forall s.\ (s \subseteq y \Rightarrow s \in U) $ | @#DDDDDD: range       | @#DDDDDD: $U$'s elements subsets are in $U$, |
| @#DDDDDD: range       | @#DDDDDD: $ \forall (y\in U).\ \exists (p\in U).\ \forall s.\ (s \subseteq y \Rightarrow s \in p) $ | @#DDDDDD: range       | @#DDDDDD: $U$'s elements power sets are in $U$, |
| @#DDDDDD: range       | @#DDDDDD: $ \forall S.\ [(S \subseteq U) \Rightarrow (S \approx_{eq} U \lor S \in U)] $ | @#DDDDDD: range       | @#DDDDDD: and $U$'s subsets of lower cardinality are in $U$. |

=== Notation II ===

Lastly some general talk about //set-builder notation//. 

When working with set theory, to abbreviate the formula $\forall z.\ [ z \in Z \Leftrightarrow (z = x \lor z = y)]$ for a certain term $Z$, we introduce the novel notation "$\{x,y\}$":

| @#EEEE55: predicate   | @#EEEE55: $X=\{a,b\}\equiv \forall c.\ ( c \in X \Leftrightarrow (c = a \lor c = b))$ |

The pairing axiom, which is taken to be true in virtually all set theories, exactly grants the existence of such a set. 

Moreover, we have "$d=\{a,b,c\}$", expressing a similar statement about //three// mathematical object and so on. The set $\{a\}\cup\{b,c\}$, which can for example be build by taking the union of the pair of pairs $\{\{a,a\}\cup\{b,c\}\}$ then also happens to fulfill exactly that defining formula, i.e.  $\{a\}\cup\{b,c\}=\{a,b,c\}$ etc.. Terms which are estabilished equal in the "$=$"-sense can be replaced for each other in a deduction.  

The axioms replacement/comprehension/collection/specification tell us to which extent the deduction of "$x\in X\Leftrightarrow P(x)$" and the associated set construction is possible within our theory. If we can specify a set by a predicate $P$, then a like sentence $X=\{x|P(x)\}$ just denotes that $X$ is the set containing the sets (in the whole domain of discourse) for which $P$ is true: 

| @#EEEE55: predicate   | @#EEEE55: $X=\{x|P(x)\} \equiv \forall x.\ (x\in X\Leftrightarrow P(x))$ |

and in that case $\forall x.\ (x\in \{x|P(x)\}\Leftrightarrow P(x))$, and then also

| @#EEEE55: predicate   | @#EEEE55: $\{ x | P(x) \} = \{ x | Q(x) \} \equiv \forall x.\ \left(P(x) \Leftrightarrow Q(x) \right).$ |

Not that $\{x|\dots$ binds (analogous to $\forall x$, $\exists x$ as well as $\lambda x$ in functional programming) and so the name $x$ is only a dummy in $\{ x | P(x) \}$. Extending the notation even more, one writes $\{f(x)|P(x)\}$ for the sets of the form $f(x)$, where $f$ is a function and the considered arguments are all the $x$, so that $P$ holds. For this we need the 2-ary abbreviation, introducing the use if function symbols as in "$f(x)$":

| @#EEEE55: predicate   | @#EEEE55: $y=f(x)\equiv \langle x,y\rangle \in f $ |

Here the notation for comprehension via functions: 

| @#FFBB00: definiendum | @#FFBB00: $\{f(x)|P(x)\} \equiv \{y|\ \exists x.\ (y=f(x)\land P(x))\}$ |

In the context of a definition section, if the domain for the terms $x$ is has been specified via $P$ before (e.g. $P(x)\equiv x\in \mathbb R$), or if the function $f$ with it's domain is already know, then we also simply write $\{f(x)\}$. Note here that $P$ is an unary predicate which "maps" the terms (in our sets-only context a.k.a. sets) to a truth or falsehood, while $f$ is a //function//, mapping sets to other sets. 

However, in set theory, functions are not primitive objects (e.g. in comparison to type theory) and formally one can't use them from the start. They are defined in the entry [[function]], which e.g. requires to be able to construct sets of [[ordered pair]]s. And when they are used like this, it is must be established that the set $f$ is, in fact, a function, i.e. it always associates two sets with each other, such that one argument-set only corresponds to one target set. 

Putting things together, we write 

| @#EEEE55: predicate   | @#EEEE55: $\{ f(x) | P(x) \} = \{ g(x) | Q(x) \} \equiv \forall y.\ \left(\exists x.\ (y=f(x) \land P(x)) \Leftrightarrow \exists z.\ \left(y=g(z) \land Q(z)\right) \right)$ |

A notable extension of the notation discussed there, which is sometimes used, is to write $\{x\in X | P(x)\}$ for $\{x | x\in X\land P(x)\}$. We'll rather avoid this, as it doesn't respect the kind of expression: $\{ x |$ and $\{ f(x) |$ contains a term and in any case $x$ is actually a bound variable. The expression $\{ x\in X |$, on the other hand, syntactically contains a proposition. The same is true for writing $\forall(x\in X).\ P(x)$ for $\forall_X x.\ P(x)$.

==== Discussion ====
=== New symbols ===
Most of what follows is concerned with demonstrating existence and uniqueness statements from the axioms and then introducing new symbols ($\emptyset, \omega_{\mathbb N}$, etc.) enabling us to use those propositions more concisely. We understand them as particular terms with particular properties, expressed by the corresponding propositions.

=== Regarding axiom systems and their strengths ===
If a logical framework (e.g. first order predicate logic, modus ponens as derivation rule) to work with has been chosen, a collections of axioms for set theory determine how to work with the binary //set membership predicate// "$\in$". 

It thereby also always //implicitly// defines a notion of "//set//": Say we are working with a specific set theory $\mathcal T$, given via a collection of axioms and consider a predicate $P$. The sentence "$\exists y.\ P(y)$" might be provable from the axioms or not. If "$\forall x.\ (x\in s \Leftrightarrow P(x))$" is a predicate on a term $s$, then the meta-sentence "$\exists y.\ P(y)$ is true" should be understood as saying "as far as the theory $\mathcal T$ is concerned, the collection of terms for which $P$ hold represent an instance of a set." 

Two theories $\mathcal T$ and $\mathcal T'$ which are defined via different existence axioms will generally not be able to agree about that meta-sentence, i.e. they might not agree if there is a set with the claimed property. 

In general, the majority of set theory axioms are about existence of certain sets. One often uses the expression "these axioms are stronger than these" to say that one theory lets one proof more sets to exists than another theory. For example [[https://en.wikipedia.org/wiki/Kripke-Platek_set_theory|Kripke-Platek set theory]] is a relatively weak set theory. A more conservative set theory is less likely to contain an inconsistency and will in general also admit less non-constructive proofs, which might be considered a pro or a con. 

=== Reference ===
Wikipedia: 
[[http://en.wikipedia.org/wiki/Implementation_of_mathematics_in_set_theory|Implementation of mathematics in set theory]],
[[http://en.wikipedia.org/wiki/List_of_first-order_theories#Set_theories|Set theories in first order logic]],
[[http://en.wikipedia.org/wiki/Tarski%E2%80%93Grothendieck_set_theory|Tarski-Grothendieck set theory]], 
[[http://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory|Zermelo–Fraenkel set theory]],

Metamath: 
[[http://us.metamath.org/mpeuni/grothprim.html|grothprim]] (Grothendieck-Tarski axiom using primitive symbols)

==== Parents ====
=== Requirements ===
[[Predicate logic]]