
> 
> Has anyone ever attempted to write down axioms capturing the behaviour of ${\bf Rel}$, the category of relations?
> 
> 
> 


Lawvere's [ETCS](https://ncatlab.org/nlab/show/ETCS) attempts to axiomatize the behaviour of the subcategory ${\bf Set}$ of ${\bf Rel}$ and ends up with a theory equiconsistent with $ZF-{\sf Replacement}$; I'm curious if axiomatizing ${\bf Rel}$ leads to a category where we can always define a subcategory corresponding to ${\bf Set}$, or if this is a second-order property not necessarily possible in 'ETCR'. If it is possible this would give ETCR at least the consistency strength of ETCS, and I'm curious if this is an upper bound on its consistency strength as well or if it's strictly stronger.



Elementary theory of the category of relations
As Sam has pointed out in the comments, [SEAR](https://ncatlab.org/nlab/show/SEAR) is close in spirit to this sort of theory. The difference is that SEAR has "elements" as a basic notion in addition to sets and relations, whereas an axiomatization of Rel would contain only sets and relations. One could in theory translate the axioms of SEAR into statements about Rel only, but the result would be rather klunky.


Probably a better thing to call "ETCR" would be to write down the axioms of a [power allegory](https://ncatlab.org/nlab/show/allegory) (also mentioned by Andreas in the comments), which is known to be equivalent to an elementary topos, and then add a suitable "well-pointed" axiom. In such a theory you would certainly always be able to isolate the "functions" from among the relations and define a category satisfying ETCS, and vice versa --- although these would of course be metatheoretic model constructions or syntactic translations rather than definitions internal to the theories.


In particular, a thus-formulated ETCR would have the same consistency strength as ETCS, namely "bounded Zermelo" a.k.a. "Mac Lane set theory". By the way, I don't think calling this "ZF $-$ Replacement" is quite right. The notion of "subtracting" an axiom (schema) from a theory is not well-defined since a theory can be axiomatized in many equivalent ways, and the result of "subtracting" some axioms depends on the whose axiomatization. In particular, if your axiomatization of "ZF" includes the full separation schema in addition to replacement, then "ZF $-$ Replacement" will be stronger than ETCS. Whereas if your axiomatization of "ZF" doesn't include any separation explicitly (instead deriving it from replacement), then "ZF $-$ Replacement" won't have any separation axiom and hence should be weaker than ETCS. There is an axiomatization of ZF such that "ZF $-$ Replacement" is equiconsistent with ETCS, namely if you include Bounded Separation explicitly in addition to the full Replacement schema, but this is not one of the usual axiomatizations of ZF.


The fact that SEAR is equiconsistent with ZF is just a choice about the default meanings of names. By default, "ETCS" does not include a replacement schema or a full separation schema, whereas by default "SEAR" does include such a schema. But you can easily add a replacement schema to ETCS to get a theory ETCS+R that's equiconsistent with ZF, or remove the replacement (actually, collection) schema from SEAR to get a theory equiconsistent with ETCS. The same would be true for any ETCR. There's a fairly extensive discussion of replacement-style axioms for categorical set theories in my paper [Comparing material and structural set theories](https://arxiv.org/abs/1808.05204v2).


