(New version appended)
Edit: I'm just trying to understand the presentations of the axioms given elsewhere. I find them a bit too "wordy" for my liking.
Can these statements be used as the axioms for category theory?
- $\forall a: Arrow(a)$
- $\forall a: Arrow(s(a))$
- $\forall a: Arrow(t(a))$
- $\forall a: s(t(a))=t(a)$
- $\forall a: t(s(a))=s(a)$
- $\forall a, b: [t(a)=s(b) \iff Arrow(comp(a,b))]$
- $\forall a, b: [Composable(a,b) \iff t(a)=s(b) \land Arrow(comp(a,b))]$
- $\forall a: comp(a,t(a))=a$
- $\forall a: comp(s(a),a)=a$
- $\forall a,b: [Composable(a,b) \implies s(a)=s(comp(a,b)) \land t(b)=t(comp(a,b))]$
- $\forall a,b,c:[Composable(comp(comp(a,b),c)), comp(a,comp(b,c)) \implies comp(comp(a,b),c)= comp(a,comp(b,c) ] $
New version incorporating some suggestions posted here...
$\forall a: [Arrow(a) \implies Arrow(s(a))]$
$\forall a: [Arrow(a) \implies Arrow(t(a))]$
$\forall a: [Arrow(a) \implies s(t(a)) = t(a)]$
$\forall a: [Arrow(a) \implies t(s(a)) = s(a)]$
$\forall a,b: [Arrow(a) \land Arrow(b) \implies [Composable(a,b) \iff t(a)=s(b)]]$
$\forall a,b: [Arrow(a) \land Arrow(b) \implies [Composable(a,b) \implies Arrow(a\circ b)]]$
$\forall a: [Arrow(a)\implies a\circ t(a)=a]$
$\forall a: [Arrow(a)\implies s(a)\circ a =a]$
$\forall a, b: [Arrow(a) \land Arrow(b) \implies [Composable(a,b) \implies s(a)=s(a\circ b) \land t(b)=t(a\circ b)]]$
$\forall a,b,c: [Arrow(a) \land Arrow(b) \land Arrow(c) \implies [Composable(a,b) \land Composable(b,c) \implies [Composable(a\circ b, c) \land Composable(a,b\circ c) \implies (a\circ b) \circ c=a\circ (b\circ c)]]]$
Comments, suggestions?
As was pointed out to you, there are several issues with your axioms.
The first one is that you must definitely remove axiom 1: if everything satisfies $Arrow$, then it is a useless predicate, and any use of it in the remaining axioms will most likely make them useless too. In the following, I will assume that axiom 1 has been removed.
My understanding is that your issue is with defining the function $comp$, since it is only defined for pairs of composable arrows, and partial functions are awkward for model theory. Your idea was to create the predicate $Arrow$ so that $comp(a,b)$ always exists, but is only declared as a valid arrow when $t(a)=s(b)$. The first obvious issue is that it means $comp(a,b)$ is completely undetermined for all other pairs of arrows, which will introduce be infinitely many non-equivalent models that should morally be equivalent.
A much more reasonable approach is to use a relation $comp(a,b,c)$ with the meaning that $c$ is the composition $b\circ a$, and axiomatize this (for instance, with an axiom stating that given $a$ and $b$, $c$ exists iff $t(a)=s(b)$, and that in that case it is unique). This is actually how you deal with partial functions: a function is just a relation with special properties, so if you want a partial function just use a relation with less constraints.
Also, I personally find it a little distasteful to define a relation in axioms: your $Composable$ is defined as a synonym of $t(a)=s(b)$, which means it can be eliminated altogether from the axioms. This is just personal taste, though.
New comment after your edit:
It is very awkward to switch the usual order of compositions: $a\circ b$ means "$b$ then $a$" for 99.9% of mathematicians, while it seems to mean "$a$ then $b$" in your axioms. It is not wrong per se, since after all the opposite category is a category, but it is at the very least confusing.
In axiom 10, $Composable(a\circ b, c)$ and $Composable(a,b\circ c)$ are actually automatic given your other axioms.
I think if you do that you get something which almost axiomatize categories.
I say "almost" because there is a lot of irrelevant data: the function $\circ$ can be anything on non-composable arrows (let alone non-arrows!), and the relation $Composable$ can be anything on non-arrows. This means that actually a model of your axioms is a little more than a category: it is a category plus some extra random data in the form of a function and a relation on a subset of the model.
If you really want to insist with your way of doing things with the $Arrow$ predicate, you should probably at least modify $Composable$ so that $Composable(a,b)$ implies that $a$ and $b$ are arrows. Modify your axiom 5 to say $$\forall a,b: [Composable(a,b)\Leftrightarrow [Arrow(a)\land Arrow(b)\land t(a)=s(b)]].$$ This makes it so $Composable$ is now fixed on the whole structure, and furthermore you don't have to repeat $Arrow(a)\land Arrow(b)$ at the beginning of every axiom, since it's included in $Composable(a,b)$.
Finally, if you want to axiomatize categories (not categories with extra random stuff), you can add a garbage constant, say $\star$, to your language, require that $\star$ is not an arrow, and send all non-composable pairs (including non-arrows) to $\star$. That way your composition is also properly fixed.
My personal opinion is that this remains much more involved than the simple solution with a $3$-ary relation as I suggested earlier, and as in Noah Schweber's comment (which gives a nice full solution).