¿Deben considerarse los axiomas como parte de la firma?

Question

Incluí la teoría de las categorías en las etiquetas para obtener comentarios de la comunidad de la lógica categorial. No hace falta decir que esto no es realmente teoría categorial.

Un semigrupo puede definirse como un modelo teórico de conjuntos $S$ de la firma

1. ordenar $U$
2. símbolo de función $f : U \times U \rightarrow U$

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

Alternativamente, podría definirse como un modelo teórico de conjuntos de la firma

1. ordenar $U$
2. símbolo de función $f : U \times U \rightarrow U$
3. axioma $\forall x,y,z \in U : f(x,f(y,z))=f(f(x,y),z).$

¿Es mejor o más correcto cualquiera de los dos enfoques? En términos más generales: ¿deben considerarse los axiomas como parte de la firma?

Answer 1

En el álgebra universal y la lógica de predicados, la firma se define esencialmente como los símbolos no lógicos. Los axiomas no forman parte de esto. Incluso la "ordenación U" no forma parte de ella, al menos para la lógica de ordenación simple predominante.

Mientras tus axiomas sean sentencias universales de Horn, tienes una noción canónica para los homomorfismos, y por tanto una conexión directa con la teoría de categorías. Una estructura común que no es una estructura universal de Horn es un conjunto totalmente ordenado. El axioma "a ≤ b o b ≤ a" no es una sentencia universal de Horn. Un remedio es basar la noción de homomorfismo en la estructura sin ese axioma. Parece que funciona, pero ¿qué pasa si se utiliza "<" en lugar de "≤" para definir los homomorfismos? Ninguno de los dos permite una axiomatización por sentencias universales de Horn, así que uno debería ser tan bueno como el otro, ¿no?

Así que mi respuesta es que los axiomas no deberían ser parte de la firma, pero que deberías intentar usar sentencias universales de Horn como axiomas (especialmente si quieres una conexión canónica con la teoría de categorías). Si no se dispone de una axiomatización con sentencias universales de Horn, hay que preguntarse qué significa esto para la categoría correspondiente, especialmente las posibles definiciones de los homomorfismos.

Answer 2

Creo que la teoría de las categorías superiores sugiere que la segunda definición es mejor. Si incluimos los axiomas en nuestros datos, esto encaja perfectamente con las categorías superiores, en las que los axiomas ya no son sólo igualdades, sino isomorfismos superiores, y estos isomorfismos deberían pertenecer a los datos. Por ejemplo, miremos la definición de una categoría monoidal (que es un monoide "superior"). La condición de asociatividad $x(yz)=(xy)z$ familiar de los monoides se sustituye por un isomorfismo de asociatividad $x(yz) \cong (xy)z$ y esto debería pertenecer a los datos. Lo que debería pertenecer a los axiomas son los condiciones de coherencia entre los isomorfismos (por ejemplo, el diagrama del pentágono en el caso de las categorías monoidales).