Beta Phase: Square45 is currently in beta testing. Expect some features or content to be incomplete or missing.
45

Axiomatic Set Theory (ZFC)

Field: Set Theory

The study of axiomatic set theory (zfc).

Sequence of Expressions

Axiom

Axioms

Includes Extensionality, Regularity, Specification, Pairing, Union, Replacement, Infinity, Power Set, and Choice.
∀A∀B(∀x(x∈A  ⟺  x∈B)  ⟹  A=B)\forall A \forall B (\forall x (x \in A \iff x \in B) \implies A = B).
Advanced
Every non-empty partially ordered set in which every chain (i.e., totally ordered subset) has an upper bound contains at least one maximal element.
∀x∀y∃z(x∈z∧y∈z)\forall x \forall y \exists z (x \in z \land y \in z).
∀F∃A∀Y∀x(x∈Y∧Y∈F  ⟹  x∈A)\forall \mathcal{F} \exists A \forall Y \forall x (x \in Y \land Y \in \mathcal{F} \implies x \in A).
∃I(∅∈I∧∀x(x∈I  ⟹  x∪{x}∈I))\exists I (\emptyset \in I \land \forall x (x \in I \implies x \cup \{x\} \in I)).
∀x∃y∀z(z⊆x  ⟹  z∈y)\forall x \exists y \forall z (z \subseteq x \implies z \in y).
Let L\text{L} be a first-order language, and let TT be a formal theory in L\text{L}. We denote Ax\text{Ax} as the set of axioms defining TT, such that T=Cn(Ax)T = \text{Cn}(\text{Ax}), where Cn(⋅)\text{Cn}(\cdot) is the closure under logical consequence. The theory TT is said to be finitely axiomatizable if there exists a finite set of formulas Ax0={A1,A2,…,Ak}k∈N\text{Ax}_0 = \{A_1, A_2, \dots, A_k\}_{k \in \mathbb{N}} such that T=Cn(Ax0)T = \text{Cn}(\text{Ax}_0). Equivalently, TT is finitely axiomatizable if there exists a finite set of axioms Ax0\text{Ax}_0 such that for every formula ϕ∈T\phi \in T, Ax0⊢ϕ\text{Ax}_0 \vdash \phi. This condition is often formalized by stating that the set of axioms Ax\text{Ax} is recursively enumerable and that TT is generated by a finite basis.