| #
|
Axiom
|
Definition
|
Comment
|
| 0
|
Existence
|
[ilmath]\exists x(x=x)[/ilmath]
|
| 1
|
Extensionality
|
[ilmath]\forall z(x\in x\leftrightarrow z\in y)\rightarrow x=y[/ilmath]
|
| 2
|
Foundation
|
[ilmath]\exists y(y\in x)\rightarrow\exists y(y\in x\wedge\not\exists z(z\in x\wedge z\in y))[/ilmath]
|
| 3
|
Comprehension schema
|
[ilmath]\exists y\forall x(x\in y\leftrightarrow x\in z\wedge\varphi(x))[/ilmath]
|
[ilmath]\varphi[/ilmath] a formula, [ilmath]y[/ilmath] not free
|
| 4
|
Pairing
|
[ilmath]\exists z(x\in z\wedge y\in z)[/ilmath]
|
| 5
|
Union
|
[ilmath]\exists A\forall Y\forall x(x\in Y\wedge Y\in\mathcal{F}\rightarrow x\in A)[/ilmath]
|
Union of [ilmath]\mathcal{F} [/ilmath]
|
| 6
|
Replacement schema
|
[ilmath]\forall x\in A\exists!y\varphi(x,y)\rightarrow\exists B\forall x\in A\exists y\in B\varphi(x,y)[/ilmath]
|
For each formula, without [ilmath]B[/ilmath] free
|
| 7
|
Infinity
|
[ilmath]\exists x(\emptyset\in x\wedge\forall y\in x(S(y)\in x))[/ilmath]
|
| 8
|
Power set
|
[ilmath]\exists y\forall z(z\subseteq x\rightarrow z\in y)[/ilmath]
|
| 9
|
Choice
|
[ilmath]\emptyset\not\in F\wedge\forall x\in F\forall y\in F(x\neq y\rightarrow x\cap y=\emptyset)\rightarrow \exists C\forall x\in F(\text{Sing}(C\cap x))[/ilmath]
|
