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: Proper class subclass of a set, via bounded separation

Nikolaj Kuntner (May 16 2024 at 16:36):

Let's consider a set theory with a restricted separation axiom - say Mac Lane or Kripke–Platek set theory, or a predicative/constructive enspired one.
(I don't know many other restricted forms of the axiom that were actually studied, but we can also tweak it more.)

What's an example of a set $a$ therin, together with a higher complexity predicate $P$, such that it's consistent that the class $\{x\in a\mid P(x)\}$ is proper, i.e. not a set, in the sense that in the theory under consideration, one may consistently adopt the negation of
$\exists p.\,\forall x.\,\left(x\in p\leftrightarrow P(x)\right)$

That $P$ must necessarily be complex enough to not be allowed in the axiom, and can't be equivalent to a low one. So I might cook up some relation of high complexity, but I don't know the set existence-independence results to make the rejection provably possible. This might be answerable in terms of absoluteness theorems studied in the Kripke–Platek.
If possible, I'd want to see a small size example, or maybe one that feels like a mathematical object that happens to not live in some category, maybe an object that MacLane set theory grants to not exist. I asked this elsewhere and the first thing that came to mind there were that it should be possible to find one among relations on the naturals, i.e. $a=\omega\times\omega$.

Mike Shulman (May 16 2024 at 21:04):

What about $a=\omega$ with $P(n) =$ "the $n$-fold iterated powerset of $\omega$ exists"? If $\{n\in \omega \mid P(n)\}$ existed for this $P$, then we could prove by induction that it is all of $\omega$, and I don't think Mac Lane set theory can prove that. You can't directly conclude from it that $\beth_\omega$ exists (which Mac Lane set theory obviously doesn't prove, even Zermelo set theory doesn't prove that) since you don't have replacement to take the image of the class-function $n\mapsto \mathcal{P}^n(\omega)$, but IIRC there is some other argument...

Mike Shulman (May 16 2024 at 21:08):

I think something of this sort appears in Mathias's paper "The strength of Mac Lane set theory".

Nikolaj Kuntner (May 16 2024 at 21:52):

Ah, yeah so Kripke-Platek set theory has Induction but not Powerset. Meanwhile Mac Lane set theory has Powerset, and I understand that the approach you take makes use of Mac Lane not being able to prove induction for sufficiently high complexity predicates. The subclass $C$ of $\omega$ defined as
$C:=\{n \in \omega \mid \text{n-iter power of w is a set} \}$
can be taken to be proper, as even the powerset characterization is $\Pi_1$.

If that checks out, negating $C$ exists as a set via that predicate about powers, we get a theory which has some model that still has $\omega$ lying around, and all finite powers of it as well, and so the initial segments of would-be $C$, and even the sets holding any finite collection of the powers of $\omega$.
My intuition for the non-existence of $C$ in that model is not great, given the finite powers exist and in all common stronger theories $C$ would just equal the existing $\omega$. :thinking emoji:

As for the other half of the paragraph, I'm not sure if you're implying reasoning about $\beth_\omega$ is actually necessary to make that argument. Indeed we can't use Replacement to get the set collecting all those powersets, but the latter is also a high rank object seemingly not necessary to talk of the non-existence of $C$.

Mike Shulman (May 16 2024 at 22:54):

If you have the set $S = \{ \mathcal{P}^n(\omega) \mid n\in \omega \}$, then you can take its union to get (a set of cardinality) $\beth_\omega$. And there's a very easy argument for why Mac Lane set theory can't construct $\beth_\omega$, namely that it has a model in $V_{\omega+\omega}$. So I was just saying that the set $C$ seems close to $S$, but unfortunately this simple argument for the nonexistence of $S$ doesn't carry over to $C$, so you need some other argument.

Nikolaj Kuntner (May 16 2024 at 22:56):

:+1: kk, so it's a good candidate but we're lacking a hard case for consistency of non-existence still

Mike Shulman (May 16 2024 at 22:56):

Check out Mathias's paper, I think it is in there somewhere.

Mike Shulman (May 16 2024 at 23:02):

My best intuition for the nonexistence of $C$ also comes from $S$, namely if you take a model of Mac Lane set theory (or even Z) that lacks $\beth_\omega$, like $V_{\omega+\omega}$, consider it as a topos, and the pass to the internal stack semantics of that topos, you get a set theory that automatically has replacement (but not full separation, even if you started with a model that had it). So replacement, which is the gap between $C$ and $S$, can kind of be added for free in a theory without full separation.

This isn't quite a proof, though, because the stack semantics also lacks excluded middle for unbounded formulas even if you started from a model that satisfies it, so it isn't quite a model of Mac Lane set theory as usually understood.