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: topos theory

Topic: Axiom of Constructibility

Fawzi Hreiki (Oct 20 2020 at 08:56):

Gödel proved that GCH and AC are equiconsistent with ZF by proving that for any model V of ZF, both statements necessarily hold in the inner model L of constructible sets. The axiom that V = L (i.e. that every set is constructible) is, properly construed, expressible in the first-order language of (material) set theory. Is there any direct analogue of this for structural set theories (like ETCS) or for toposes more generally?

Fawzi Hreiki (Oct 20 2020 at 08:58):

My first thought is that we can require that any propositional function, i.e. any map into the subobject classifier, is the finite composite of more basic definable propositional functions (whatever those happen to be)

Fawzi Hreiki (Oct 20 2020 at 09:22):

For reference, the Wikipedia page on the constructible universe, https://en.wikipedia.org/wiki/Constructible_universe, is fairly comprehensive (no pun intended)

David Michael Roberts (Oct 20 2020 at 10:29):

I've been interested for a long time whether we can define things like inner models (like $L$ inside $V$) in structural set theory (see eg https://mathoverflow.net/questions/190757/existence-of-internal-toposes-inner-models-in-a-topos). I've never gotten a good answer!

Fawzi Hreiki (Oct 20 2020 at 15:04):

Is there a way to define what it would mean for a propositional function $X \rightarrow \Omega$ in a topos to be finitary first-order (either via the internal language or externally)?

Morgan Rogers (he/him) (Oct 20 2020 at 18:00):

Each of the operations permissible in the construction of these first order sentences can be made categorical, right? So it seems feasible at first glance?

Fawzi Hreiki (Oct 20 2020 at 20:11):

Well yeah, because in a topos, all the logical operations internalise to the sub object classifier

Fawzi Hreiki (Oct 20 2020 at 20:11):

And when the topos is well pointed, we know that the internal logic corresponds exactly to what can be said about it externally

Fawzi Hreiki (Oct 20 2020 at 20:13):

Well modulo some stuff about quantification scope

Morgan Rogers (he/him) (Oct 21 2020 at 09:23):

There aren't many well-pointed toposes, I would avoid that constraint :relieved:

Morgan Rogers (he/him) (Oct 21 2020 at 09:28):

We could actually hash this out here; it seems like you know enough between you about inner models to work out what the construction should look like, and it wouldn't be the first example of finding one topos within another (in a sense other than a subtopos). Whenever the subobject classifier is a finite object, the class of finite objects in a topos is itself a topos; it would be interesting to have a topos of "constructible objects" within any given topos.

Fawzi Hreiki (Oct 21 2020 at 11:55):

Well, you're right that most toposes aren't well pointed, but the whole point of $L$ is that it's objects (namely, the constructible sets) are even more static than those in ambient universe of sets $V$. The point is to, at least at first, mirror the construction of $L$ but from a category satisfying ETCS. I can't imagine a scenario where one is interested in the definable subobjects (whatever that means) in a topos which is not understood as a topos of abstract sets (e.g. in a non-trivial sheaf topos).

Morgan Rogers (he/him) (Oct 21 2020 at 12:11):

Any topos can be viewed/understood as a topos of abstract sets, though.

Morgan Rogers (he/him) (Oct 21 2020 at 12:13):

To do anything inductive/infinite, you need a natural number object, so that's likely to be necessary for determining definable subobjects, but I don't see why well-pointedness would be necessary.

Morgan Rogers (he/him) (Oct 21 2020 at 12:19):

The problem I have when looking at the Constructible Universe page is that I don't understand the definition of Def(X); if someone could clarify that for me, maybe we could make some progress.

John Baez (Oct 21 2020 at 15:57):

I find Wikipedia's formal definition of Def(X) confusing for certain reasons, but I know it's trying to say something like this. You're working in a universe a la material set theory, and then for any set X you want to create a set Def(X) of all subsets of X that are "definable in terms of elements of X".

My confusion arises from this:

1) In the text they say Def(X) is a collection of subsets of X. They call Def(X) a "stage" and X "the previous stage", and they say:

In Gödel's constructible universe L, one uses only those subsets of the previous stage that are:

• definable by a formula in the formal language of set theory,
• with parameters from the previous stage and,
• with the quantifiers interpreted to range over the previous stage.

This is actually pretty clear except that "definable" needs to be fleshed out. But in their formula for Def(X) they say it's a collection of elements of X. This can't be right, I think, since it would force Def(X) $\subseteq$ X, contradicting the whole goal of building up bigger and bigger "stages". Does everyone here agree?

2) Given the set $X$, they say $x$ is "definable" if there are elements $y_1, \dots, y_n \in X$ ("parameters") and a first order-formula $\Phi$ in the language of ZF such that $\Phi(x,y_1, \dots , y_n)$ holds when all quantifiers are interpreted in $X$.

What's weird about this is that many different $x$ could obey $\Phi(x,y_1, \dots , y_n)$, so I don't see how this captures the idea that $x$ is being defined. E.g. we could take $\Phi$ to be tautologously true, and then every $x$ would be "defined" in this way.

Oscar Cunningham (Oct 21 2020 at 16:01):

In the formula for $\mathrm{Def}(X)$ they don't say that it's made up of elements of $X$, they say it's made up of sets whose elements are elements of $X$.

Dan Doel (Oct 21 2020 at 16:02):

Where does it say that Def(X) is a collection of elements of X? The formula has two nestings of braces, which is a little hard to notice at first. So I think that makes the elements subsets?

Oscar Cunningham (Oct 21 2020 at 16:03):

And this makes sense of (2) too. If we take $\Phi$ to be a tautology, then it defines the set $X$, which we do want to be part of $\mathrm{Def}(X)$.

John Baez (Oct 21 2020 at 16:03):

Yes, that extra brace changes everything. It solves both my problems.

John Baez (Oct 21 2020 at 16:03):

We're not talking about definable elements of X; we're talking about definable subsets of X.

John Baez (Oct 21 2020 at 16:04):

So, I hope my confusion, and its correction, will help @[Mod] Morgan Rogers get what's going on here.

John Baez (Oct 21 2020 at 16:06):

I don't think I've ever seen nested set-builder notation like

$\{ \{x : x \in y \} : y \in Y \}$

before, and I clearly haven't had enough coffee - I probably assumed I was just seeing double, as usual early in the morning.

Oscar Cunningham (Oct 21 2020 at 16:06):

So in the case of structural set theory would we define $\mathrm{Def}$ to take a subcategory of a topos to a larger subcategory containing the things that can be defined from it?

John Baez (Oct 21 2020 at 16:11):

That's a thing you could try. But that seems like it could expand really fast. One thing we have in material set theory is

$\mathrm{Def}(X) \subseteq P(X)$

If instead of $\mathrm{Def}(X)$ we used $P(X)$ to get the "next stage", we'd inductively build up the von Neumann hierarchy:

$V_{\alpha + 1} = P(V_\alpha)$

The constructible hierarchy

$L_{\alpha + 1} = \mathrm{Def}(L_\alpha)$

is a kind of "refinement" of the von Neumann hierarchy.

So, we could ask if there's anything like the von Neumann hierarchy in topos theory!

John Baez (Oct 21 2020 at 16:15):

But maybe there isn't, in which case Oscar's idea seems best (to me, a total amateur).

Dan Doel (Oct 21 2020 at 16:55):

Not every $V_α$ is a topos, right? So doing every step as a topos is probably skipping a lot of steps.

Morgan Rogers (he/him) (Oct 21 2020 at 16:57):

A universe of sets (a la Grothendieck in SGA4, say) is required to be closed under the basic operations of set construction, notably including the powerset. That is, if we take it to be "all sets less than some cardinality $\alpha$" in some model of set theory, we require that for all $\kappa < \alpha$ we have $2^{\kappa} < \alpha$.

Morgan Rogers (he/him) (Oct 21 2020 at 16:58):

So, while we have to assume that an infinite such cardinality exists to have any universe at all beyond the finite sets, once we do, a full von Neumann hierarchy fits into it, and the definable subobjects should be... definable within the topos.

Dan Doel (Oct 21 2020 at 16:59):

It seems like I've seen a $V_α$ for toposes somewhere, but I don't remember where exactly. Maybe one of the papers on stack semantics or something?

Dan Doel (Oct 21 2020 at 17:01):

It might have been similar to what you do in type theory, too. In a structural set theory, you can define a construction of trees that act like material sets, and talk about $V_α$ there or something.

Dan Doel (Oct 21 2020 at 17:01):

But that might not be exactly what is desired, I don't know.

Morgan Rogers (he/him) (Oct 21 2020 at 17:11):

John Baez said:

So, I hope my confusion, and its correction, will help [Mod] Morgan Rogers get what's going on here.

The problem I have is that I'm not familiar enough with the formal language of set theory to know what a first-order formula consists of, which is what one would need to know in order to internalise this construction into a general topos.

John Baez (Oct 21 2020 at 17:15):

By "first- order formula in the language of ZF" I mean any formula whatsoever one can write down with logical connectives, variables, quantifiers, equals signs, and $\in$.

John Baez (Oct 21 2020 at 17:18):

If it helps, forget that I said "first-order". This was not a limiting adjective: it's just a reminder that ZF is formulated in plain old classical logic - the logic that ordinary logicians use.

Dan Doel (Oct 21 2020 at 17:18):

I guess an obvious question is, "why use ZF?" Doesn't exactly seem appropriate for all toposes.

John Baez (Oct 21 2020 at 17:21):

Since people defined the constructible universe using ZF, we have to understand that case a teeny bit before we try to generalize it to topoi. That's all.

Morgan Rogers (he/him) (Oct 21 2020 at 17:23):

Except there are some caveats about the quantifiers here, right?

John Baez (Oct 21 2020 at 17:30):

The formula $\Phi$ I mentioned is any formula whatsoever with $n+1$ free variables. In $\Phi(x,z_1, \dots, z_n)$ we require that $z_1, \dots, z_n$ are specific elements of $X$. But most importantly, in Wikipedia's definition

$\mathrm{Def}(X) := \Bigl\{ \{ y \mid y \in X \text{ and } (X,\in) \models \Phi(y,z_1,\ldots,z_n) \} ~ \Big| ~ \Phi \text{ is a first-order formula and } z_{1},\ldots,z_{n} \in X \Bigr\}$

the $(X,\in) \models \Phi(y,z_1,\ldots,z_n)$ thing means that $\Phi(y,z_1,\ldots,z_n)$ is satisfied in $X$ - that is, when we check for satisfaction, all variables take values in $X$, and $\in$ is interpreted using the actual $\in$ relation.

John Baez (Oct 21 2020 at 17:35):

In this definition $(X, \in)$ doesn't need to be a model of ZF. For example, when we build the constructible hierarchy we start by letting $X$ be the empty set; that's our set $L_0$, and then we define higher $L_\alpha$'s inductively via

$L_{\alpha + 1} = \mathrm{Def}(L_\alpha)$

and the obvious thing at limit ordinals. Only when $\alpha$ is an inaccessible cardinal does $(L_\alpha, \in)$ actually get to be model of ZF. Note that $L_\omega$ is already a topos. It's also a model of ZF minus the axiom of infinity.

Morgan Rogers (he/him) (Oct 21 2020 at 17:41):

Trying to re-express this in categorical language is funny, because I have to try to express $Def(X)$ constructively as a subobjects of $\Omega^X$. Making positive statements, like that if $A$ and $B$ are in $Def(X)$ then their union must also be, is easy, but I can't see how to get more precise than that yet (basically, I'm able to identify some necessary properties of the classifying map, but so far there is no way to distinguish $Def(X)$ from $\Omega^X$. On the other hand, that might just be topos theory telling me that I can't tell that a subset is 'not definable' in a constructive way)

John Baez (Oct 21 2020 at 17:44):

You might prefer to start with the nLab definition of the constructible hierarchy, which is presumably equivalent to the usual one, though I'm not sure why.

Dan Doel (Oct 21 2020 at 18:04):

They look like rough correspondences of various axioms. Maybe finite axiomatization of NBG would help, too, but I can't find an actual list of the finite axioms.

Dan Doel (Oct 21 2020 at 18:07):

'Domain of a binary relation' sounds like it might be similar to replacement.

Fawzi Hreiki (Oct 21 2020 at 19:17):

John Baez said:

You might prefer to start with the nLab definition of the constructible hierarchy, which is presumably equivalent to the usual one, though I'm not sure why.

Those operations listed on the nLab are the so-called 'Godel operations'. Its a theorem (see ch. 13 of Jech's book) that the two definitions are equivalent but its certainly not trivial why.

Morgan Rogers (he/him) (Oct 21 2020 at 20:35):

Haha the real question is how constructive the equivalence is :yum: I'll take a detailed look tomorrow.

Fawzi Hreiki (Oct 21 2020 at 20:40):

When it comes to high powered ZF stuff, the answer is almost always "not at all"

David Michael Roberts (Oct 21 2020 at 21:31):

I hope everyone realises that the inclusion $L \hookrightarrow V$ induces a faithful, essentially surjective functor between the corresponding categories of sets. The real trick is in cutting down the hom-sets, since only functions with definable graphs can be used.

David Michael Roberts (Oct 21 2020 at 22:01):

Dan Doel said:

It seems like I've seen a $V_α$ for toposes somewhere, but I don't remember where exactly. Maybe one of the papers on stack semantics or something?

It appears in Algebraic Set Theory, by Joyal and Moerdijk. Also in Awodey, Butz, Simpson, Streicher "Relating first-order set theories, toposes and categories of classes". The latter is somewhat related to stack semantics, but only secretly.

David Michael Roberts (Oct 21 2020 at 22:03):

Note also that even the tautological-looking ZFC theorem $V = \bigcup_{\alpha} V_\alpha$ may not hold in slightly weaker set theories. Bounded Zermelo, which is the material version of ETCS, can't prove it, for instance. See eg https://mathoverflow.net/questions/363598/does-bounded-zermelo-construct-any-cumulative-hierarchy

Dan Doel (Oct 21 2020 at 22:04):

Well, I probably didn't read it in those, because I haven't actually read those. But I guess there are a lot of places to read about it. :)

David Michael Roberts (Oct 21 2020 at 22:06):

Yeah, probably in some older papers relating material and structural set theories. What are other papers on stack semantics other than Mike Shulman's preprint? I mean proper stack semantics, not just the Kripke–Joyal stuff that involves bounded quantifiers that's been around for ages.

Dan Doel (Oct 21 2020 at 22:06):

Well, it was most likely something by Mike Shulman.

Dan Doel (Oct 21 2020 at 22:07):

I read a bunch of his set theory stuff at random.

Fawzi Hreiki (Oct 21 2020 at 22:13):

Yeah you could probably do everything with algebraic set theory but that kind of defeats the purpose since you're back with the cumulative hierarchy. The idea is to try and define this subcategory $L(\mathscr{E}) \hookrightarrow \mathscr{E}$ without passing through the hierarchy.

Morgan Rogers (he/him) (Oct 22 2020 at 07:46):

David Michael Roberts said:

I hope everyone realises that the inclusion $L \hookrightarrow V$ induces a faithful, essentially surjective functor between the corresponding categories of sets. The real trick is in cutting down the hom-sets, since only functions with definable graphs can be used.

This is definitely something I would not have guessed that is very good to know!

John Baez (Oct 22 2020 at 16:21):

Yes! - it amounts to saying every cardinal is in $L$.