Is the theory of regular formal languages finitely axiomatizable?

Suppose, $$A$$ is a countable alphabet. Define the class of regular languages in the following recursive way:

$$\emptyset \in Reg$$

$$\forall a \in A \text{ } \{a\} \in Reg$$

$$\forall L_1, L_2 \in Reg \text{ } L_1 \cup L_2, L_1 L_2 , \langle L_1 \rangle := \bigcup_{n \in \mathbb{N}} L_1^n \in Reg$$

According to this definition, $$Reg$$ is closed under $$\cup$$ (union), $$\cdot$$ (formal language product) and $$\langle … \rangle$$ (formal language iteration).

Suppose $$T_{Reg}$$ is the first-order theory with equality of $$Reg$$, with three functions: binary $$\cup$$ and $$\cdot$$ and unary $$\langle … \rangle$$

Is $$T_{Reg}$$ finitely axiomatizable?

I have a feeling, that it isn't, but do not know how to prove it.

• Yes, look at Kleene algebra – hermes Dec 15 '19 at 0:18
• Don't you want to also include $\{\varepsilon\}\in \text{Reg}$, where $\varepsilon$ is the empty word? – Alex Kruckman Dec 15 '19 at 4:20

Maybe a more natural question is whether the equational theory of $$\text{Reg}$$ is finitely axiomatizable (motivated by the goal of understanding when two regular expressions define the same language). My understanding is that the answer is no, and this was proven by Redko in 1964. But a finite axiomatization of the universal Horn theory of $$\text{Reg}$$ was given by Kozen in 1994 (in the language with the three function symbols you give, together with constant symbols $$0$$ for $$\emptyset$$ and $$1$$ for $$\{\varepsilon\}$$, where $$\varepsilon$$ is the empty word). As pointed out by MathWizard in the comments, a model of this universal Horn theory is called a Kleene algebra, and $$\text{Reg}$$ is the free Kleene algebra on generators $$A$$.

Ok, but you asked about the complete first-order theory $$T$$ of $$\text{Reg}$$. I will show that this theory is not finitely axiomatizable as follows:

If $$T$$ is finitely axiomatizable, so is $$T_c$$, the complete theory of $$\text{Reg}$$ with a new constant symbol $$c$$ naming $$\{a\}$$ for some $$a\in A$$ ($$T_c$$ is axiomatized by adding one new axiom to $$T$$). It follows that $$T_c$$ is decidable (since it is complete and finitely axiomatizable). But $$T_c$$ interprets the true theory of arithmetic, so it cannot be decidable, by Gödel's theorem.

Note that this argument actually proves something stronger: $$T$$ is not even recursively axiomatizable.

Here are some preliminary observations:

• The subset relation on languages is definable by $$x\subseteq y$$: $$x\cup y = y.$$
• The empty language is definable by $$\text{empty}(x)$$: $$\forall y\, (x\cup y = y).$$
• The language $$\{\varepsilon\}$$ is definable by $$\text{null}(x)$$: $$\forall y\, (x\cdot y = y).$$
• The set of singleton languages $$\{l\}$$ is definable by $$\text{sing}(x)$$: $$\forall y\, \forall z\, ((y\cup z = x)\rightarrow (\text{empty}(y)\lor y = x))$$
• Among singleton languages, the ones that consist of a single character $$\{a\}$$ with $$a\in A$$ are definable by $$\text{char}(x)$$: $$\text{sing}(x)\land \forall y\, \forall z\, ((y\cdot z = x)\rightarrow (\text{null}(y)\lor y = x)).$$

Now suppose that $$T$$ is finitely axiomatizable. If we add a new constant symbol $$c$$ to the language and interpret it in $$\text{Reg}$$ as $$\{a\}$$ for some $$a\in A$$, then I claim that the complete theory of this structure is axiomatized by $$T_c = T\cup \{\text{char}(c)\}$$. Indeed, note that if $$\text{Reg}\models \text{char}(l)$$ for some other language $$l$$, we have $$l = \{a'\}$$ with $$a'\in A$$. And the permutation of $$A$$ which swaps $$a$$ and $$a'$$ extends to an automorphism of $$\text{Reg}$$. Thus the formula $$\text{char}(x)$$ isolates the complete type of $$\{a\}$$ in $$\text{Reg}$$, so $$T_c$$ is a complete theory.

We can now move on to interpreting arithmetic in $$T_c$$. The domain of the interpretation is the set $$\{\{\varepsilon\},\{a\},\{aa\},\{aaa\},\dots\}$$, where $$\{a^n\}$$ will represent the natural number $$n$$. This set is defined by $$\text{dom}(x)$$: $$\text{sing}(x)\land (x\subseteq \langle c\rangle).$$

We can easily define addition on this set by concatenation: $$a^n\cdot a^m = a^{n+m}$$.

We can also define the divisibility relation $$x\mid y$$ by $$y\subseteq \langle x\rangle,$$ since if $$x = \{a^n\}$$ and $$y = \{a^m\}$$, then $$\{a^m\}\subseteq \langle \{a^n\}\rangle = \{a^{kn}\mid k\in \mathbb{N}\}$$ if and only if $$m = kn$$ for some $$k\in \mathbb{N}$$.

Now it's a theorem of Julia Robinson's that multiplication is definable in the structure $$(\mathbb{N},+,|)$$. In fact, it's enough to just have the successor function $$S(x)$$ (which in our copy of arithmetic is defined by $$x\cdot c$$) and the divisibility relation. See Theorem 1.2 in Robinson's paper Definability and Decision Problems in Arithmetic. So we have shown that $$T_c$$ interprets the true theory of arithmetic, as desired.