Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Is ETCS a two-sorted first order theory?

Suraaj K S (Dec 28 2024 at 09:11):

I've been reading Tom Leinster's course notes on Axiomatic Set theory, which treats ETCS as the foundational theory, rather than ZFC. We know that ZFC is a single sorted first order theory, with the one sort being for 'sets', and one binary predicate ∈ for membership (This is all we need if I understand correctly. Although perhaps one could also give a theory with a nullary operation for empty set, etc.)

My question is about ETCS, as described in the lecture notes. I think that the theory is not single sorted - there are 'things' which are sets, and there are 'things' which are functions too. I do think that ETCS is a multisorted first-order theory, though. My question is: what precisely would be the sorts, predicates, and operators for ETCS?

Suraaj K S (Dec 28 2024 at 09:17):

Well, I guess, we don't even need to go to ETCS. Perhaps the essence of the question is just about 'the theory of categories'

Oscar Cunningham (Dec 28 2024 at 09:17):

The most natural way to do it is to say the objects have one sort, and then for each pair of objects, $A$ and $B$, there's a sort $\mathrm{Hom}(A,B)$ of functions from $A$ to $B$. The operator $\mathrm{Hom}$ is a 'dependent sort'. The extremely relevant paper is First Order Logic with Dependent Sorts, with Applications to Category Theory.

Suraaj K S (Dec 28 2024 at 09:19):

Oscar Cunningham said:

The most natural way to do it is to say the objects have one sort, and then for each pair of objects, $A$ and $B$, there's a sort $\mathrm{Hom}(A,B)$ of functions from $A$ to $B$. The operator $\mathrm{Hom}$ is a 'dependent sort'. The extremely relevant paper is First Order Logic with Dependent Sorts, with Applications to Category Theory.

I see, so the doctrine / underlying logic for the theory would not be first-order logic.

Oscar Cunningham (Dec 28 2024 at 09:24):

Perhaps not first-order logic as it's usually defined. But any theory with dependent sorts can be made into an equivalent one without, in this case by putting all the morphisms in a single sort like you said originally, and then having a predicate that says when $f$ is a morphism from $A$ to $B$. So all the usual theorems about first-order logic still hold.

Suraaj K S (Dec 28 2024 at 09:37):

Oscar Cunningham said:

Perhaps not first-order logic as it's usually defined. But any theory with dependent sorts can be made into an equivalent one without, in this case by putting all the morphisms in a single sort like you said originally, and then having a predicate that says when $f$ is a morphism from $A$ to $B$. So all the usual theorems about first-order logic still hold.

I see. In this case, the 'theory of categories' would be a 2-sorted first-order theory (one sort for objects, another sort for morphisms).

I'm wondering if you'd define the composition operation as a binary operation on the sort of morphisms? In this case, it seems like there can be many 'ill-typed' terms. How does one enforce that domains and codomains match?

Oscar Cunningham (Dec 28 2024 at 09:42):

Yes, an advantage of dependent sorts is that you don't have to worry about these ill-typed terms. In the 2-sorted theory it would probably be easiest to just have a predicate '$f$ is the composite of $g$ and $h$' which is false when $g$ and $h$ aren't compatible.

Vincent R.B. Blazy (Dec 28 2024 at 11:13):

Suraaj K S said:

I'm wondering if you'd define the composition operation as a binary operation on the sort of morphisms? In this case, it seems like there can be many 'ill-typed' terms. How does one enforce that domains and codomains match?

Another equivalence of FOLDS or Generalized FOL is with Essentially First-Order Logic (usually seen only in the Algebraic Theories case, with GATs vs. EATs), which does not have "dependent" sorts (I.e. non-atomic sorts formed from Terms) but rather partial function symbols! That gives you the composition one :blush:

Spencer Breiner (Dec 28 2024 at 13:48):

Probably worth noting that categories can also be defined without reference to objects, with identities standing in (due to Freyd), e.g., here: https://math.stackexchange.com/questions/17469/category-theory-with-and-without-objects

Todd Trimble (Dec 28 2024 at 13:51):

More directly, [[single-sorted definition of categories]]. I'm not absolutely sure it's due to Freyd, but it might be. It appears in Categories for the Working Mathematician. (Edit: Apparently also in Freyd's Abelian Categories, which now makes me think it is due to Freyd -- sorry I seemed to be doubtful a few sentences ago.)

Mike Shulman (Dec 28 2024 at 16:53):

FOLDS as formulated by Makkai doesn't actually have function symbols, only relation symbols. He had a good reason for doing it that way, but it sort of defeats part of the purpose here since you still have to encode composition by a relation instead of a dependently typed function $\hom(y,z) \times \hom(x,y) \to \hom(x,z)$. Unfortunately I don't know of a place where "dependently typed first-order logic" that does include function symbols is written down precisely, but it should be easy to do.

Patrick Nicodemus (Dec 30 2024 at 15:36):

@Suraaj K S did you look at the paper?
http://www.tac.mta.ca/tac/reprints/articles/11/tr11.pdf

Patrick Nicodemus (Dec 30 2024 at 15:37):

ETCS is a first-order theory with a single sort called the sort of "mappings". The object x is identified with the identity morphism id_x.

Patrick Nicodemus (Dec 30 2024 at 15:39):

composition is a partially defined function, which it is easy to model as a ternary relation on morphisms: $R(f, g, h)$ holds if $g\circ f=h$