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.

  • 5
    $\begingroup$ Are you aware of ncatlab.org/nlab/show/SEAR ? $\endgroup$ Nov 26, 2022 at 3:37
  • 5
    $\begingroup$ 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. $\endgroup$ Nov 26, 2022 at 3:39
  • $\begingroup$ @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. $\endgroup$
    – Alec Rhea
    Nov 26, 2022 at 3:40
  • $\begingroup$ @AndreasBlass Thank you for the pointer, I'll see if I can find a copy. $\endgroup$
    – Alec Rhea
    Nov 26, 2022 at 3:41

1 Answer 1


As Sam has pointed out in the comments, 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 (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.

  • $\begingroup$ Thank you Mike, if nothing else crops up as competition in the next few days I’ll accept this answer. $\endgroup$
    – Alec Rhea
    Nov 26, 2022 at 8:44
  • 3
    $\begingroup$ I really wish there was a paper on SEAR, not "just" an nlab page. I quite like this theory as a foundation. $\endgroup$ Nov 26, 2022 at 11:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.