# Elementary theory of the category of relations

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

Lawvere's 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.

• Are you aware of ncatlab.org/nlab/show/SEAR ? Nov 26, 2022 at 3:37
• I suggest looking into the book "Categories, Allegories" by Freyd and Scedrov. If I remember correrctly, the notion of allegory is intended to capture the essential properties of Rel. Nov 26, 2022 at 3:39
• @SamHopkins I'm aware of structural set theories, but I haven't looked into SEAR specifically. After a glance it seems interesting; if a structural set theory focusing on sets, elements and relations is equiconsistent with ZF then perhaps ETCR (whatever the appropriate first order theory of the category of relations is) is equiconsistent with ZF as well. Nov 26, 2022 at 3:40
• @AndreasBlass Thank you for the pointer, I'll see if I can find a copy. Nov 26, 2022 at 3:41

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.