# Category formulas without explicit specifying of objects

Consider the following example:

$C$ is a category each of whose Hom-sets is partially ordered. Let $f$, $g$, and $h$ are morphisms of this category. Consider the formula: $g\circ f \ge h$.

Intuition suggests that from this formula it follows:

1. $f$ and $g$ are composable that is the destination of $f$ is the source of $g$.
2. $g\circ f$ and $h$ lie in the same Hom-set, that is the source of $f$ is the same as the source of $h$ and destination of $g$ is the same as the destination of $h$.

So, intuition suggests that these conditions 1 and 2 follow from the formula. But can we define it formally, in order not to say explicitly that these equalities (1 and 2) of sources and destination hold? It is very boring to formulate such conditions explicitly in every statement about morphisms in a category.

-
You can define in your introduction the meaning of the term "whenever it makes sense". For example "$f\circ (g\circ h)=(f\circ g)\circ h$ whenever it makes sense" could then appear as part of the definition of category. On the other hand, what yuold you wish to be the meaning of $\neg(f\circ g\ge h)$? –  Hagen von Eitzen Sep 25 '12 at 13:39

For a given (first order) similarity type $t$, one can introduce so called first order 'situations', as a pair $\langle X,\Gamma\rangle$ where $X$ is a (finite) set of variables, and $\Gamma$ is a set of atomic formulas over $X$. An interpretation of this in a modell $M$ is just an evaluation $u:X\to M$ such that $M\models\Gamma[u]$.

Among partial algebras, an interpretation $u$ of $\langle X,\Gamma\rangle$ is effectively meant such that for all equation $"\sigma(\bar x)=\tau(\bar x)"\,\in\Gamma$, the evaluated terms $\sigma(u(\bar x))$ and $\tau(u(\bar x))$ are defined and equal.

So, in this sense, the interpretations of your $\langle\{f,g,h\},\{"f\circ g\le h"\} \rangle$ may already include the wished hypothesis.

How to say, this all can be viewed as it is only about a good phrasing in the preface of a book/paper.

-
What is "similarity type"? –  porton Sep 25 '12 at 18:49
a set $Sym$ of function and relation symbols equipped with the arity function $Sym\to\mathbb N$. Now you have one binary (partial) operation and one binary relation. –  Berci Sep 25 '12 at 19:09

If you want to be explicit, you can do it for example as follows: Let $C$ be a category whose homsets are ordered by relations $\le_{A,B}$ on each $\mathrm{Hom}_C(A,B)$. Define a relation $\le$ on the class $\operatorname{Mor}C$ by $f \le g :\!\iff \exists A,B \in \operatorname{Obj}C,\> f,\!g: A \to B \wedge f \le_{A,B} g$

-
Not good. In this case $a \nleq b$ would be not equivalent to $\neg \left( a \leq b \right)$. –  porton Sep 25 '12 at 13:48
Why. IMO $a \not\le b$ is by definition $\neg(a \le b)$ ... if I define only $\le$ as above. –  martini Sep 25 '12 at 15:40
We could define $r^\ast$ for a relation $r$ as $f r^\ast g\iff \exists A,B\in\operatorname{Obj} C, f,g:A\rightarrow B\land f r g$. –  porton Sep 25 '12 at 15:45
Then $\neg(a\leq^\ast b)$ would be not the same as $a\nleq^\ast b$ –  porton Sep 25 '12 at 15:46