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: Algebraic theory of two elements?

Mike Stay (Apr 22 2021 at 17:23):

Is there a way to have an algebraic theory of a set with at least two elements? Just pointing twice doesn't work, because there are models where the two point function symbols pick out the same element of the set. If not, what's the weakest kind of theory that allows you to say "these two points are distinct"?

John Baez (Apr 22 2021 at 17:26):

Every algebraic theory has the 1-element set as its terminal model, right?

The overall moral is that you can't express inequalities in a Lawvere theory, a prop, an algebraic theory, or even an essentially algebraic theory. Negation is a fairly high-powered concept. We get it in a topos, for sure, since in a Heyting algebra we can define not(P) as "P implies false". I don't know the answer to your second question, though: the weakest kind of theory that allows you to express inequalities.

Mike Shulman (Apr 22 2021 at 17:41):

I would say, the internal language of a category with finite limits and a strict initial object. This is like coherent logic, but with only $\bot$ and not $\vee$.

Spencer Breiner (Apr 22 2021 at 17:42):

Not really an answer, but the question reminds me a bit of the dual logic in this paper:
https://arxiv.org/abs/0902.1950
It builds up the (dual) logical theory of quotients starting from the notion of a distinction or "dit".

John Baez (Apr 22 2021 at 17:46):

Mike Shulman said:

I would say, the internal language of a category with finite limits and a strict initial object.

Nice! What goes wrong if your initial object isn't strict? Negation gets sort of funny then...

(For those not in the know, "strict" means that any object $x$ with a morphism $x \to 0$ is itself initial.)

Mike Shulman (Apr 23 2021 at 02:40):

Well, the idea would be that when interpreting predicates in the subobject fibration, we use the initial object for bottom elements of the posets of subobjects. Strictness ensures that those bottom elements are stable under pullback. You get pretty weird "logic" if you start giving up preservation of connectives under substitution.