<p>I am reading the <a href="http://dl.acm.org/citation.cfm?id=321326" rel="noreferrer">classical article</a> of A. Salomaa where he gives two axiom systems for regular sets and proofs consistency and completeness.</p>

<p>As I have understood it, an axiomatic system in some logic (lets suppose predicate first order logic) are axioms formulated in the language of the logic, i.e. well-formed formulas together with primitive notions (constant, predicate or function symbols). And a (set theoretical) model is an interpretation for this.</p>

<p>For example, consider the theory of groups. The <a href="https://en.wikipedia.org/wiki/Primitive_notion#cite_note-5" rel="noreferrer">primitive notions</a> are groups, multiplication, inversion and idenity, mostly written as $(G, \cdot, ^{-1}, 1)$ and the axioms would be
\begin{align*}
 &amp; \forall x,y,z : (xy)z = x(yz) \\
 &amp; \forall x \exists y : xy = 1 \\
 &amp; \forall x : x1 = x \land 1x = x.
\end{align*}
The existence of certain groups shows its consistency, and as there are models such that for example the sentence $\forall x \forall y : xy = xy$
is either true or false, it is not complete. But essential here is that when talking about the theory we have just the axioms in mind, without bearing to any actual realisation/model.</p>

<p>Now to come back to Salomaa's paper, in his system $F_1$ he lists $11$ Axioms. Now it is easy to see that regular expression (defined as terms over some alphabet) are a model for these axioms, but besides that their might be other models. When dealing with questions about this axiom system in general we cannot argue with one specific model, or?</p>

<p>To be more specific, in Lemma 4 of his paper he shows that every regular expression has an equational characterisation (i.e. a set of equations this expression fulfills) and this is essential for the completeness proof. And the proof goes by induction over the construction of regular expression, so it works just for this specific model. But in fact he must how that everything (not just regular expressions) obeying the axioms have such an equational characterisation, so he must argue more general than using the specific model of regular expression?</p>

<p>Am I right? Or why does this works out... or am I confusing something here, in what sense does regular expressions go into the axiom system that we can use this model in proving statements about the axiom system (I guess this is not the only model, or?).</p>

CC BY-SA 3.0
2017-04-14T11:30:09.113Z
I can't access the paper so I don't really know but: Yes, there may be other models, like there are other models of Peano in first order logic. But non-standard models of Peano all contain the standard model (meaning that there is a subset of each non-standard model that's isomorphic to the standard model to them). I'd guess that that's what he's proving here: All models of his theory contain a subset isomorphic to the "standard" model: regular expressions.
xavierm02
CC BY-SA 3.0
2017-04-14T11:35:44.557Z
If the axioms are "algebraic", it's probably equivalent to proving that for any given model, there is an injective morphism from regular expressions to any the model, which he seems to describe by giving a set of equations characterizing the image of a regular expression by the morphism. And it's perfectly fine to define a function from regular expressions to something else by induction on regular expressions. (You can sometimes prove everything in one model, but only after you've proved that all other models are isomorphic to it. And the theory of a model is always complete)
xavierm02
<lo.logic><fl.formal-languages><regular-expressions><formal-systems>
Salomaa's axiomatisation of regular languages and the use of regular expression in it
StefanH
# Salomaa's axiomatisation of regular languages and the use of regular expression in it

(Asked by: username_0 on 2017-04-13)

I am reading the [classical article](http://dl.acm.org/citation.cfm?id=321326) of A. Salomaa where he gives two axiom systems for regular sets and proofs consistency and completeness.

As I have understood it, an axiomatic system in some logic (lets suppose predicate first order logic) are axioms formulated in the language of the logic, i.e. well-formed formulas together with primitive notions (constant, predicate or function symbols). And a (set theoretical) model is an interpretation for this.

For example, consider the theory of groups. The [primitive notions](https://en.wikipedia.org/wiki/Primitive_notion#cite_note-5) are groups, multiplication, inversion and idenity, mostly written as $(G, \cdot, ^{-1}, 1)$ and the axioms would be
\begin{align\*}
& \forall x,y,z : (xy)z = x(yz) \\
& \forall x \exists y : xy = 1 \\
& \forall x : x1 = x \land 1x = x.
\end{align\*}
The existence of certain groups shows its consistency, and as there are models such that for example the sentence $\forall x \forall y : xy = xy$
is either true or false, it is not complete. But essential here is that when talking about the theory we have just the axioms in mind, without bearing to any actual realisation/model.

Now to come back to Salomaa's paper, in his system $F\_1$ he lists $11$ Axioms. Now it is easy to see that regular expression (defined as terms over some alphabet) are a model for these axioms, but besides that their might be other models. When dealing with questions about this axiom system in general we cannot argue with one specific model, or?

To be more specific, in Lemma 4 of his paper he shows that every regular expression has an equational characterisation (i.e. a set of equations this expression fulfills) and this is essential for the completeness proof. And the proof goes by induction over the construction of regular expression, so it works just for this specific model. But in fact he must how that everything (not just regular expressions) obeying the axioms have such an equational characterisation, so he must argue more general than using the specific model of regular expression?

Am I right? Or why does this works out... or am I confusing something here, in what sense does regular expressions go into the axiom system that we can use this model in proving statements about the axiom system (I guess this is not the only model, or?).

**Tags:** lo.logic, fl.formal-languages, regular-expressions, formal-systems
> **Comments:**
> **username_1**: I can't access the paper so I don't really know but: Yes, there may be other models, like there are other models of Peano in first order logic. But non-standard models of Peano all contain the standard model (meaning that there is a subset of each non-standard model that's isomorphic to the standard model to them). I'd guess that that's what he's proving here: All models of his theory contain a subset isomorphic to the "standard" model: regular expressions.  
> **username_1**: If the axioms are "algebraic", it's probably equivalent to proving that for any given model, there is an injective morphism from regular expressions to any the model, which he seems to describe by giving a set of equations characterizing the image of a regular expression by the morphism. And it's perfectly fine to define a function from regular expressions to something else by induction on regular expressions. (You can sometimes prove everything in one model, but only after you've proved that all other models are isomorphic to it. And the theory of a model is always complete)  

---

## 0 answers

