I am reading the classical article 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 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?).