y
z
(z
x
z
y
).
Axiom ZF1 - Sets with the same members are equal - (Extensionality).
If x and y are sets then x
y
z
(zx
zy
).
Axiom ZF2 - The "Empty Set" is a set. We write it as
There exists a set
such that
x(
(x
)).
Note by ZF1
is unique.
Axiom ZF3 - Set Formation - Unordered Pairs.
If x,y are sets then there exists a set z such that
a
(a
z
(a
x or a
y)).
We write this unique set as {x,y} . Note that {x,x} which is the same as {x} is not the set x.
Axiom ZF4 - Set Formation - Selection.
If
z,y
,y
,
...,
y
are sets and
is a proposition
containing variables
and a free variable
and doesn't contain other free variables then
there exits a set y such that
x(x
y
(x
z
and
)
).
Note that this avoids Russell's Paradox since we require x to be a member of a "known set." Again, it is unique.
Translation:We write
y
{x
z
\
}.
Axiom ZF5 - Set Formation - Union.
If x is a set then there exists a set y such that
a
(a
y
(
z( z
x
and
a
z)
).
Translation: We
write y
x
, or some variant thereof
Axiom ZF6 - Set Formation - Power set.
If x is a set then there exists a set z such that
y(
y
z
(
a
(a
y
a
y
) ).
Translation: (
a
(a
y
a
y
) is just a definition of
inclusion y
x
Axiom ZF7 - There is an infinite set
There exists a set m such that
m
and
x(x
y
(
({x,{x}})
m).
Translation:
({x,{x}}
is the set containing all the members of x and the set
x itself.
Axiom ZF8 - Replacement( Functional Image)
Let
be
a proposition that does not contain the symbol b then
x
y
y
(
(
x
y
and
x
y
)
y
y
)
a
b
c ( c
b
d(d
a
and \Phi
d
c))
).
Translation: If, given any set x, there is a unique set
y such that
x
y
,
then, given any set a, there is a set b such
that, given any set c, c is a member of
b if and only if there is a set d such that
d is a member of a and
\Phi holds for d and
c.
Axiom ZF9 - There are not Russell's Paradox like Sets (Regularity).
If x is a set and x
then
y
(y
x
and
a
(
(a
x
and
a
y)).
Translation: Every non-empty set contains a member that does not any members in common with it.
Note
a(
(a
x
and
a
y)).
can be read
x
y
.
This can be shown to rule out the Russell set.