[proofplan]
A rewrite system on $\Omega$ is determined by its finite rule set $P \subseteq \Omega^\star \times \Omega^\star$, so the set of rewrite systems embeds into $\operatorname{Fin}(\Omega^\star \times \Omega^\star)$. We show the latter is countable by chaining three facts: (i) $\Omega^\star$ is countable because $\Omega$ is finite and hence countable; (ii) the Cartesian product of two countable sets is countable; (iii) the set of finite subsets of a countable set is countable. All three are established theorems on Androma.
[/proofplan]
[step:Reduce to counting finite subsets of $\Omega^\star \times \Omega^\star$]
By definition, a rewrite system on $\Omega$ is a pair $(\Omega, P)$ where $P \subseteq \Omega^\star \times \Omega^\star$ is a finite set of rules. With $\Omega$ fixed, the rewrite system is determined by $P$ alone, so the set of rewrite systems on $\Omega$ is in bijection with
\begin{align*}
\operatorname{Fin}(\Omega^\star \times \Omega^\star) &= \{P \subseteq \Omega^\star \times \Omega^\star : P \text{ is finite}\}.
\end{align*}
It therefore suffices to show that $\operatorname{Fin}(\Omega^\star \times \Omega^\star)$ is countable.
The reduction is worth pausing on: the *pair* $(\alpha, \beta) \in \Omega^\star \times \Omega^\star$ is the minimal piece of data a single rewrite rule must record, so the codomain $\Omega^\star \times \Omega^\star$ is the natural ambient set for rules. Finiteness of $P$ is part of the definition — a rewrite system is allowed only finitely many rules, consistent with the finite-description ethos of formal language theory.
[/step]
[step:Show that $\Omega^\star$ is countable]
Since $\Omega$ is finite, $\Omega$ is countable (a finite set admits a surjection from $\mathbb{N}$, for instance the map sending $1, \dots, |\Omega|$ bijectively to $\Omega$ and $k \mapsto $ (any fixed element) for $k > |\Omega|$). If $\Omega = \varnothing$ then $\Omega^\star = \{\varepsilon\}$ is a singleton, hence finite and countable. Otherwise $\Omega$ is nonempty and countable, so by the [Countability of $X^\star$](/theorems/1774) applied with $X := \Omega$, the set $\Omega^\star$ is countable (and in fact countably infinite).
The finiteness of $\Omega$ matters twice in the chain.
First, it makes $\Omega$ countable at all — without finiteness we would need an external hypothesis of countability on $\Omega$.
Second, in the informal reading of the argument, one can replace the general countability result with the concrete enumeration of $\Omega^\star$ in shortlex order: fix a total order on $\Omega$ and list strings by length, breaking ties lexicographically.
The shortlex enumeration gives an explicit bijection $\mathbb{N} \to \Omega^\star$ whenever $\Omega$ is finite and nonempty, sharper than the prime-factorisation argument used in the general theorem. We cite the general theorem here for uniformity with later chapters that work over infinite alphabets.
[/step]
[step:Show that $\Omega^\star \times \Omega^\star$ is countable]
Let $\sigma_1, \sigma_2: \mathbb{N} \to \Omega^\star$ be surjections; one such $\sigma$ exists by the previous step, and we take $\sigma_1 = \sigma_2 = \sigma$. By the [Countability of Finite Cartesian Products](/theorems/???) (equivalently, the countability of $\mathbb{N} \times \mathbb{N}$ via the Cantor pairing map), define
\begin{align*}
\varphi: \mathbb{N} &\to \Omega^\star \times \Omega^\star \\
k &\mapsto (\sigma(k_1), \sigma(k_2)),
\end{align*}
where $(k_1, k_2) \in \mathbb{N} \times \mathbb{N}$ is the image of $k$ under a fixed bijection $\mathbb{N} \to \mathbb{N} \times \mathbb{N}$ (e.g., the Cantor pairing function). Given $(u, v) \in \Omega^\star \times \Omega^\star$, surjectivity of $\sigma$ yields $a, b \in \mathbb{N}$ with $\sigma(a) = u$, $\sigma(b) = v$, and surjectivity of the Cantor pairing yields $k \in \mathbb{N}$ with $(k_1, k_2) = (a, b)$, giving $\varphi(k) = (u, v)$. Hence $\varphi$ is surjective and $\Omega^\star \times \Omega^\star$ is countable.
[/step]
[step:Conclude that $\operatorname{Fin}(\Omega^\star \times \Omega^\star)$ is countable]
Set $Y := \Omega^\star \times \Omega^\star$. From the previous step $Y$ is countable. By the [Countability of Finite Subsets](/theorems/1775) applied with $X := Y$, the set $\operatorname{Fin}(Y) = \operatorname{Fin}(\Omega^\star \times \Omega^\star)$ is countable. Combined with the reduction in the first step, there are at most countably many rewrite systems on $\Omega$.
The countability bound is sharp whenever $\Omega$ is nonempty: the map sending each finite set $F \subseteq \Omega^\star$ to the rewrite system with rule set $\{(\varepsilon, \alpha) : \alpha \in F\} \cup \{(\alpha, \alpha) : \alpha \in F\}$ is an injection from $\operatorname{Fin}(\Omega^\star)$ into the set of rewrite systems on $\Omega$, and $\operatorname{Fin}(\Omega^\star)$ is countably infinite (infinitely many singleton subsets, each a distinct element). Hence the set of rewrite systems on a nonempty $\Omega$ is countably infinite — the countability bound is attained, not merely an upper bound.
This quantitative fact has a qualitative consequence at the level of languages: since each grammar is built from a rewrite system plus a finite auxiliary structure (terminal/nonterminal split, start symbol), there are at most countably many grammars and hence at most countably many grammar-generated languages — whereas the set of all languages $\mathcal{P}(\mathbb{W})$ is uncountable by [Cantor's Theorem](/theorems/621). Most languages are not grammar-generated, and a fortiori not computable. This is the first precise cardinality-based non-existence result in the course.
[/step]
