Como se te ha señalado, hay varios problemas con tus axiomas.
La primera es que hay que eliminar definitivamente el axioma 1: si todo satisface $Arrow$ entonces es un predicado inútil, y cualquier uso que se haga de él en los axiomas restantes probablemente también los hará inútiles. En lo que sigue, supondré que el axioma 1 ha sido eliminado.
Entiendo que tu problema es con la definición de la función $comp$ ya que sólo se define para pares de flechas componibles, y las funciones parciales son incómodas para la teoría de modelos. Tu idea era crear el predicado $Arrow$ para que $comp(a,b)$ siempre existe, pero sólo se declara como flecha válida cuando $t(a)=s(b)$ . La primera cuestión obvia es que significa $comp(a,b)$ es completamente indeterminado para todos los demás pares de flechas, lo que introducirá ser infinitamente muchos modelos no equivalentes que debe ser moralmente equivalentes.
Un enfoque mucho más razonable es utilizar una relación $comp(a,b,c)$ con el significado de que $c$ es la composición $b\circ a$ y axiomatizarlo (por ejemplo, con un axioma que establezca que dado $a$ y $b$ , $c$ existe si $t(a)=s(b)$ y que en ese caso es único). En realidad, así es como se tratan las funciones parciales: una función no es más que una relación con propiedades especiales, así que si quieres una función parcial sólo tienes que utilizar una relación con menos restricciones.
Además, personalmente encuentro un poco desagradable definir una relación en axiomas: su $Composable$ se define como sinónimo de $t(a)=s(b)$ lo que significa que puede eliminarse por completo de los axiomas. Aunque esto es sólo gusto personal.
Nuevo comentario después de tu edición:
-
Es muy incómodo cambiar el orden habitual de las composiciones: $a\circ b$ significa " $b$ entonces $a$ " para el 99,9% de los matemáticos, mientras que parece significar " $a$ entonces $b$ "en sus axiomas. No es incorrecto per se, ya que al fin y al cabo la categoría opuesta es una categoría, pero como mínimo es confuso.
-
En el axioma 10, $Composable(a\circ b, c)$ y $Composable(a,b\circ c)$ son en realidad automáticas dados sus otros axiomas.
Creo que si haces eso obtienes algo que casi axiomatiza las categorías.
Digo "casi" porque hay muchos datos irrelevantes: la función $\circ$ puede ser cualquier cosa sobre flechas no componibles (¡y mucho menos sobre flechas no componibles!), y la relación $Composable$ puede ser cualquier cosa en las no flechas. Esto significa que, en realidad, un modelo de sus axiomas es algo más que una categoría: es una categoría más algunos datos aleatorios adicionales en forma de una función y una relación sobre un subconjunto del modelo.
Si de verdad quieres insistir con tu forma de hacer las cosas con el $Arrow$ probablemente debería modificar al menos $Composable$ para que $Composable(a,b)$ implica que $a$ y $b$ son flechas. Modifica tu axioma 5 para que diga $$\forall a,b: [Composable(a,b)\Leftrightarrow [Arrow(a)\land Arrow(b)\land t(a)=s(b)]].$$ Esto hace que $Composable$ se fija ahora en toda la estructura, y además no hay que repetir $Arrow(a)\land Arrow(b)$ al principio de cada axioma, ya que está incluido en $Composable(a,b)$ .
Finalmente, si quieres axiomatizar categorías (no categorías con cosas aleatorias extra), puedes añadir una constante basura, digamos $\star$ a su idioma, exigen que $\star$ no es una flecha, y enviar todos los pares no componibles (incluyendo los que no son flechas) a $\star$ . De esta forma también se fija correctamente la composición.
Mi opinión personal es que esto sigue siendo mucho más complicado que la simple solución con un $3$ -ary como sugerí antes, y como en el comentario de Noah Schweber (que da una bonita solución completa).
