Zermelo–Fraenkel set theory

**Zermelo–Fraenkel set theory** (abbreviated **ZF**) is a standard system of rules used to describe set theory. These rules are known as axioms, which are statements that do not need to be proven. When the axiom of choice is added to ZF, the system is called **ZFC**.  It is the system of axioms used in set theory by most mathematicians today.

After Russell's paradox was found in 1901, mathematicians wanted to find a way to describe set theory that did not have contradictions.  Ernst Zermelo proposed a theory of set theory in 1908.  In 1922, Abraham Fraenkel proposed a new version based on Zermelo's work, which would become ZF.

ZF set theory is written using the language of first order logic with an extra symbol. Although ZF is about sets, there are ways to convert other math statements into statements about sets. Then, we can write a math sentence such as "1+1=2" in this language, and prove it using only the axioms of ZF. Because this language is very precise, it's possible to ask metamathematical questions, and prove statements about what can and can't be proved in ZF.

## Axioms
An axiom is a statement which is accepted without question and which has no proof. ZF traditionally contains eight axioms. Two of these axioms (specification and pairing) are redundant, as they can be deduced from the axiom schema of replacement. Nevertheless, these extra axioms are useful; replacement is rarely used for proving theorems in common mathematics.

# The **axiom of extension** says that two sets are equal if and only if they have the same elements. For example, the set \{1, 3\} and the set \{3, 1\} are equal.
# The **axiom of foundation** says that every set S (other than the empty set) contains an element that is disjoint (shares no elements) with S. This means that no set can contain itself.
# The **axiom of specification** says that given a set S, and a predicate F (a function that is either true or false), a set exists that contains exactly those elements of S where F is true.  For example, if S = \{1, 2, 3, 5, 6\}, and F is "this is an even number", then the axiom says that the set \{2, 6\} exists. This can be deduced from the replacement axiom.
# The **axiom of pairing** says that given two sets, there is a set whose elements are exactly the two given sets.  So, given the two sets \{0, 3\} and \{2, 5\}, this axiom says that the set \{\{0, 3\}, \{2, 5\}\} exists.
# The **axiom of union** says that for any set, there exists a set that consists of just the elements of the elements of that set.  For example, given the set \{\{0, 3\}, \{2, 5\}\}, this axiom says that the set \{0, 3, 2, 5\} exists.
# The **axiom of replacement** says that for any set S and a function F, the set consisting of the results of applying the function F to every element of S exists (also known as range or image). For example, if S = \{1, 2, 3, 5, 6\} and F is "add ten to this number", then the axiom says that the set \{11, 12, 13, 15, 16\} exists.
# The **axiom of infinity** says that the set of all non-negative integers (as defined by the von Neumann construction) exists. This is the set \{0, 1, 2, 3, 4, ...\}.
# The **axiom of power set** says that for any set S, the power set of S exists (the set of all of the subsets of S). For example, the power set of \{2, 5\} is \{\{\}, \{2\}, \{5\}, \{2, 5\}\}. The empty set and the set S itself are considered subsets of S.

## Axiom of choice
The **axiom of choice** says that for any set S, where the empty set is not an element of S, there exists a function F whose domain is S, such that F(E) is an element of E for any element E of S. For example, given the set S = \{\{0, 3\}, \{2, 5\}\}, the axiom of choice asserts the existence of a function that "picks" exactly one element from each of the elements of S (in this case S has two elements), but it doesn't tell us what combination it is. For finite sets, this axiom can be proved from the other axioms, but not for infinite sets.

## References
* 
* 
*