Should axioms be viewed as part of the signature?

Question

I included category theory in the tags in order to get feedback from the categorial logic community. It goes without saying that this isn't really category theory.

A semigroup can be defined as a set-theoretic model $S$ of the signature

1. sort $U$
2. function symbol $f : U \times U \rightarrow U$

such that $$S \models \forall x,y,z \in U : f(x,f(y,z))=f(f(x,y),z).$$

Alternatively, it could be defined as a set-theoretic model of the signature

1. sort $U$
2. function symbol $f : U \times U \rightarrow U$
3. axiom $\forall x,y,z \in U : f(x,f(y,z))=f(f(x,y),z).$

Is either approach better or more correct? More generally: should axioms be viewed as part of the signature?

Answer 1

In universal algebra and predicate logic, the signature is essentially defined as the non-logical symbols. The axioms are not part of this. Even "sort U" is not part of this, at least for the prevalent single-sorted logic.

As long as your axioms are universal Horn sentences, you have a canonical notion for homomorphisms, and hence a direct connection to category theory. A common structure which is not a universal Horn structure is a totally ordered set. The axiom "a ≤ b or b ≤ a" fails to be a universal Horn sentence. One remedy is to base the notion of homomorphism on the structure without that axiom. It seems to work, but what if you use "<" instead of "≤" for defining homomorphisms? Neither one allows an axiomatization by universal Horn sentences, so one should be as good as the other, no?

So my answer is that axioms should not be part of the signature, but that you should try to use universal Horn sentences as axioms (especially if you want a canonical connection to category theory). If no axiomatization with universal Horn sentences is available, you should ask yourself what this means for the corresponding category, especially the possible definitions of homomorphisms.

Answer 2

I think that higher category theory suggests that the second definition is better. If we include axioms into our data, this fits smoothly with higher categories where axioms are not just equalities anymore, but rather higher isomorphisms, and these isomorphisms should belong to the data. For example, look at the definition of a monoidal category (which is a "higher" monoid). The associativity condition $x(yz)=(xy)z$ familiar from monoids is replaced by an associativity isomorphism $x(yz) \cong (xy)z$, and this should belong to the data. What should belong to the axioms are the coherence conditions between the isomorphisms (for example the pentagon diagram in the case of monoidal categories).