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: deprecated: logic

Topic: elementary embeddings

John Baez (Nov 22 2020 at 20:49):

Maybe some of you can help me answer this question from Harvey Friedman:

Greetings!

I'm looking at certain semigroups G = (G,dot). And I use the notion
from logic of an elementary embedding j from G into G. This means that
for any first order statement phi over (G,dot) with parameters from G,
phi holds in (G,dot) if and only that holds after we replace those
parameters with their values under j.

Semiformally, we can write

phi(g1,...,gk) if and only if phi(j(g1),...,j(gk)).

My question is this. Is there a nice and interesting categorical
reformulation of this notion; i.e., elementary embeddings, from the
categorical point of view? And has it figured much in category theory?

Thanks,

Harvey

John Baez (Nov 22 2020 at 20:55):

I have ideas about this, but I'd be interested to hear yours. The stuff about semigroups is not the main point, I think, nor is the fact that we have an elementary embedding of something into itself. I think the real question is: how should we think about elementary embeddings in first-order logic using category theory? The nLab article is useful:

• Elementary embeddings.

John Baez (Nov 22 2020 at 20:58):

If I don't hear from any of you, I guess I'll just try to explain this article to Friedman.

Nathanael Arkor (Nov 22 2020 at 20:59):

As I understand it, this is very much tied into the theory of accessible categories. Beke–Rosický's Abstract elementary classes and accessible categories could be a good place to start.

John Baez (Nov 22 2020 at 21:17):

I think accessible categories are too fancy - that is, too specialized - to get to the heart of this question. As the nLab page points out (especially in the conversation between Mike Shulman and Urs Schreiber), the concept of "structure", "model" and "elementary embedding" are very general category-theoretic concepts, which apply in many different doctrines.

John Baez (Nov 22 2020 at 21:18):

It sounds like accessible categories are important for certain specific questions in model theory, as in Rosický's talk next Friday.

John Baez (Nov 22 2020 at 21:21):

But the nLab page points out that an elementary embedding is quite generally a natural transformation where the naturality squares are pullbacks.

Fawzi Hreiki (Nov 22 2020 at 21:23):

I know that Lurie’s notes on categorical logic have some stuff on elementary embeddings as they relate to syntactic categories

সায়ন্তন রায় (Nov 23 2020 at 03:54):

@John Baez This is an extremely interesting question. I have two comments,

• I completely agree with you that, "The stuff about semigroups is not the main point, I think, nor is the fact that we have an elementary embedding of something into itself."

• I believe a more interesting and deeper question is, how should we think about homomorphisms $j$ between two structures $C$ and $D$ in first-order logic (well, we may probably replace this by other logics as well) which is such that $\varphi(g_1,\ldots g_k)$ implies $\varphi(j(g_1),\ldots j(g_k))$ using category theory.

I am wondering whether adjoint functors can be seen via some notions related to the notion of homomorphisms already mentioned.

John Baez (Nov 23 2020 at 17:04):

Sayantan Roy said:

• I believe a more interesting and deeper question is, how should we think about homomorphisms $j$ between two structures $C$ and $D$ in first-order logic (well, we may probably replace this by other logics as well) which is such that $\varphi(g_1,\ldots g_k)$ implies $\varphi(j(g_1),\ldots j(g_k))$ using category theory.

I agree that this feels like the more fundamental concept. I guess logicians would call this an "embedding", since they typically work with a language where you can choose $g_1 \ne g_2$ as your predicate $\varphi(g_1,g_2)$, and this would imply $j(g_1) \ne j(g_2)$.

Oscar Cunningham (Nov 23 2020 at 17:33):

If we have $\phi(g)\rightarrow\phi(j(g))$ for all $\phi$ then we also have $\phi(j(g))\rightarrow\phi(g)$ by substituting $¬\phi$ for $\phi$.

Dan Doel (Nov 23 2020 at 17:40):

I don't have that.

Oscar Cunningham (Nov 23 2020 at 17:45):

Because it's not constructive?

Dan Doel (Nov 23 2020 at 17:45):

Yes.

Dan Doel (Nov 23 2020 at 17:55):

That might mean that you can't just use negation, though. Although I'm not sure how everything is quantified.

Dan Doel (Nov 23 2020 at 17:57):

For instance, if you pick $\phi(g) = \psi(g) → \psi(h)$ then you can get $\psi(j(h)) → \psi(h)$.

John Baez (Nov 23 2020 at 21:45):

By the way: I'm going to try to explain this to Harvey Friedman, and he doesn't give a damn about dropping the law of excluded middle or anything like that. He only cares about classical logic, and I know better than to argue with him about that. (Besides, I think classical logic is an interesting subject.)

Peter Arndt (Nov 24 2020 at 00:59):

One aspect is this: Elementary embeddings make all set comprehensions become functorial.

If you have a formula, it defines a subset of every structure, in a uniform way, but this is not a functor from structures and homomorphisms to sets: For example given a ring homomorphism $f: R \to S$ we don't get an induced map $\{x \in R \mid \neg \exists y: xy=1\} \to \{x \in S \mid \neg \exists y: xy=1 \}$ because non-units can become units in the codomain ring. The culprit here is negation; other examples can be constructed for example with $\forall \exists$-formulas, where the culprit is the quantifier alternation.

A class of formulas that do induce functors is the class of positive primitive formulas, i.e. those of the form $\exists x (\varphi_1 \wedge \ldots \wedge \varphi_n)$ with atomic formulas $\varphi_i$. But those don't allow to express many things.

So a way to allow more expressive formulas and have those induce functors is to restrict the class of morphisms. On the extreme end you allow all formulas but are left only with elementary embeddings. [But actually elementary morphisms would be enough for this -- see the nlab page on elementary embeddings -- so I guess this really is a better justification for the elementary morphisms than for the embeddings...]

সায়ন্তন রায় (Nov 24 2020 at 04:51):

@Peter Arndt You need to enclose your math by $$. :stuck_out_tongue:

Peter Arndt (Nov 24 2020 at 14:07):

Corrected, thanks! :grimacing:

John Baez (Nov 24 2020 at 17:10):

Nice, thanks!