Theorem·T57
A countable language has countably many formulas
If a language's own function and relation symbols are countable, so is its alphabet, and so are its formulas.
For a language
with
:
In words
For a language whose function and relation symbols are both countable: its set of formulas is countable.
Never needed: F10 · F13 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).
Proof
- 1
- 2A finite union of countable sets is countable: pairwise, if are countable with injections into , then if , else , is an injection (the tag vs , paired via pi, keeps the two cases from colliding); iterating over the four pieces, is countable.
- 3
∎
Remarks
The alphabet argument for
mirrors T53 one level down (a fixed, finite number of pieces rather than
-many, so a direct pairwise argument suffices without invoking Choice again). This is exactly what licenses enumerating
as
(some injection into
, extended - if
is infinite, which it always is - to a surjection back out by repeating any one formula past the injection's range), the raw material the Lindenbaum construction recurses over.