Skip to content
Axiomatic Wiki
Theorem·T56

Finite sequences from a countable set are countable

All finite sequences from a countable set, of any length, still only countably many.

For a countable set :
In words
For a countable set X: the set of all finite sequences from X, of every length, is countable.
Rests onF02F03F04F05F06F08F09F11F12F14A01A02A06A08A09
Never needed: F10 · F13 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).

Proof

  1. 1
    By D074 and D085: - every has for some , i.e. , and conversely every member of some is a member of .
  2. 2
    By T55, is countable for every . By T53 (applied to the function , domain ): is countable, i.e. is countable.
∎

Remarks

The payoff of the whole countability chain: since a language's alphabet is countable whenever its function and relation symbols are (a finite union, , of countable pieces), terms and formulas - both subsets of - are countable too, by this theorem together with downward closure of countability under subsets. This is exactly the enumeration Lindenbaum's lemma needs to build a maximal consistent extension by simple -recursion.
Wikipedia ↗Set.Countable ↗

Used by

T57
Propose an edit1 published revision