nLab axiom of union

The axiom of union

The axiom of union

Idea

In material set theory as a foundation of mathematics, the axiom of union is an important axiom needed to get the foundations off the ground (to mix metaphors). It states that unions exist.

Statement

Β In material set theory

The axiom of union states the following:

Axiom (union)

If 𝒳\mathcal{X} is a (material) set, then there exists a set UU such that a∈Ua \in U whenever a∈Bβˆˆπ’³a \in B \in \mathcal{X}.

Using the axiom of separation (bounded separation is enough), one can prove the existence of a particular set UU such that the members of the members of 𝒳\mathcal{X} are the only members of UU. Using the axiom of extensionality, we can then prove that this set UU is unique; it is usually denoted ⋃𝒳\bigcup\mathcal{X} and called the union of (the elements of) 𝒳\mathcal{X}.

A slightly different notation may be used when 𝒳\mathcal{X} is (Kuratowski)-finite; for example, ⋃{A,B,C}\bigcup\{A,B,C\} may be denoted AβˆͺBβˆͺCA \cup B \cup C. If (B k|k∈I)(B_k \;|\; k \in I) is a family of sets, then we may write ⋃ k∈IB k\bigcup_{k \in I} B_k (and the usual variations for a sequence of sets) for ⋃{B k|k∈I}\bigcup \{B_k \;|\; k \in I\}; however, we require the axiom of replacement to prove that the latter set (the range of the family) exists in general.

Β In dependent type theory

In dependent type theory, it is possible to define a Tarski universe (V,∈)(V, \in) of pure sets which behaves as a material set theory. The universal type family of the Tarski universe is given by the type family x:VβŠ’βˆ‘ y:Vy∈xx:V \vdash \sum_{y:V} y \in x. The axiom of union is given by the following inference rule:

Ξ“ctxΞ“βŠ’union V:∏ x:Vβˆ‘ U:V∏ y:V∏ z:V(y∈x)Γ—(z∈y)β†’(z∈U)\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{union}_V:\prod_{x:V} \sum_{U:V} \prod_{y:V} \prod_{z:V} (y \in x) \times (z \in y) \to (z \in U)}

There is a similar axiom for binary unions:

Ξ“ctxΞ“βŠ’union V:∏ x:V∏ y:Vβˆ‘ U:V∏ z:V((z∈x)β†’(z∈U))Γ—((z∈y)β†’(z∈U))\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{union}_V:\prod_{x:V} \prod_{y:V} \sum_{U:V} \prod_{z:V} ((z \in x) \to (z \in U)) \times ((z \in y) \to (z \in U))}

With the type theoretic axiom of choice, this is equivalent to the axiom

Ξ“ctxΞ“βŠ’union V:βˆ‘ (βˆ’)βˆͺ(βˆ’):VΓ—Vβ†’V∏ x:V∏ y:V∏ z:V((z∈x)β†’(z∈xβˆͺy))Γ—((z∈y)β†’(z∈xβˆͺy))\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{union}_V:\sum_{(-) \cup (-):V \times V \to V} \prod_{x:V} \prod_{y:V} \prod_{z:V} ((z \in x) \to (z \in x \cup y)) \times ((z \in y) \to (z \in x \cup y))}

If 𝒳\mathcal{X} is given as a collection of subsets of some ambient set SS, then the axiom of union is not necessary; SS itself already satisfies the conclusion of the hypothesis (and then bounded separation gives us the union that we want). This is the only case when unions are taken in structural set theory. However, structural set theory makes use of disjoint unions, and predicative mathematics requires an axiom giving their existence. (In impredicative mathematics, we can construct disjoint unions from power sets and cartesian products.)

One could also include union structure in the set theory.

Last revised on February 28, 2024 at 04:23:17. See the history of this page for a list of all contributions to it.