natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
(a countable union of countable sets is countable, aka the countable union theorem)
Assuming the axiom of countable choice then:
Let $I$ be a countable set and let $\{S_i\}_{i \in I}$ be an $I$-dependent set of countable sets $S_i$. Then the disjoint union
is itself a countable set.
Classical proof: we may assume all the $S_i$ are nonempty. For each $i \in I$, choose a surjection $f_i: \mathbb{N} \to S_i$ (this requires the axiom of countable choice) and also a surjection $f: \mathbb{N} \to I$. Then we have a composite surjection
where for $pair: \mathbb{N} \to \mathbb{N} \times \mathbb{N}$ we may take for example the function that is inverse to $(x, y) \mapsto \binom{x+y+1}{2} + y$.
For constructive mathematicians who accept the axiom of countable choice, the proof is only slightly more elaborate. Here we define a set to be countable if it is a quotient of (is enumerated by) a decidable subset, i.e., a complemented subobject of $\mathbb{N}$. Thus, supposing we have chosen surjections out of decidable subsets $(f_i: J_i \to S_i)_{i \in I}$, and a surjection $J \to I$ out of a decidable subset $J$, we have a diagram (switching to $\sum$ to denote disjoint sums)
whose limit might be denoted $\sum_{j \in J} K_j$ where $K_j \coloneqq J_{f(j)}$. This is certainly a complemented subobject of $\mathbb{N}$, the complement being formed as $\left(\sum_{j \in J} \neg K_j\right) + (\neg J) \cdot \mathbb{N}$, and the limit obviously maps surjectively onto $\sum_{i \in I} S_i$, as desired.
The implication countable choice $\Rightarrow$ countable union theorem cannot be reversed, as there are models of ZF where the latter holds, but countable choice fails. Further, the countable union theorem implies countable choice for countable sets, but this implication also cannot be reversed.
Countable Unions And The Axiom Of Countable Choice, MathOverflow discussion
Last revised on April 26, 2019 at 12:41:04. See the history of this page for a list of all contributions to it.