Timeline for What are some interesting hyperdoctrines that are not classical models?
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 5, 2021 at 21:49 | vote | accept | So8res | ||
| Oct 5, 2021 at 21:49 | comment | added | So8res | This isn't quite fully concrete, but it's near enough that I feel like it answers my original question. (One takeaway I have extracted so far is that hyperdoctrines can interpret theories into multiple model-like structures plus relationships between them, in a particular technical sense.) And fwiw, I'm personally sold on constructive logic (and I'm a least somewhat familiar with the cool new interpretations it brings), but I'm still curious about what hyperdoctrines bring to the classical table :-). Thanks again! | |
| Oct 5, 2021 at 21:45 | comment | added | So8res | Ok, so IIRC: Let T be a theory with models including Newtonian-mechanics-style configurations. Suppose T is "transformation invariant" in the sense that for every model and element of SO(3) (or whatever), we have a corresponding transformed model. In the traditional framework, we see a whole host of models plus some "invariance theorems" describing how syntax commutes with transformation. In categorical semantics, the whole host and its relativity theorems from a single hyperdoctrine, which also does a bunch of the commuting-theorem legwork using the general machinery of interpretation. Neat! | |
| Oct 5, 2021 at 19:26 | comment | added | Mike Shulman | Another big class of Boolean examples is double-negation sheaves on forcing posets. This yields, in particular, forcing models of ZFC in the classical sense. So in particular this way you get a hyperdoctrine for ZFC that violates the continuum hypothesis. | |
| Oct 5, 2021 at 19:25 | comment | added | Mike Shulman | You get a lot more interesting examples if you generalize to constructive logic. Then you can use, for instance, the category of sheaves on any topological space, or the category of presheaves on any small category. For classical logic, I agree that set-indexed powers of sets are not all that interesting. I think $\rm Set^{core(Set)}$ is a bit too big to be very interesting, but ${\rm Set}^G$ for a group $G$ is interesting: the objects are sets with a $G$-action, the subsets are sub-actions. So you are doing "equivariant mathematics" for any group of equivariance. | |
| Oct 5, 2021 at 15:38 | comment | added | So8res | (Meta: I plan to keep chewing on this, and if I manage to find a concrete example, I'll be satisfied. In the interim, I'd continue to appreciate assistance; I still feel like so far all I've got is generic descriptions of where the "new non-model hyperdoctrines" hang out, rather than a concrete example that shows off the generality of hyperdoctrines. If I'm being daft and there's an obvious non-trivial specific example here, please do let me know.) | |
| Oct 5, 2021 at 15:37 | comment | added | So8res | So what does the hyperdoctrine of subobjects in Set^Set look like? We could interpret a formula w/ n free variables as a subobject of (const U^n ∈ Set^Set). Which is essentially a groupoid homomorphism (F : Set^Set) paired with an injective transformation to (const U^n). The components of the transformation are like, for every set A, an injection from F(A) to U^n. So an interpretation for a formula is a sort of natural family of subobjects. The remaining Q is to find an actual interpretation of some theory (eg, PA) into Sub(Set^Set), that isn't just the boring one (where F is always constant). | |
| Oct 4, 2021 at 21:42 | comment | added | So8res | Attempting to work out a concrete example using this idea... Letting $X = 2$, I could pick any two traditional models of PA, and sew together a hyperdoctrine that interprets each formula into the corresponding pair of sets. But that doesn't quite feel "new and interesting" to me. On the other extreme, letting $X = \mathrm{Set}$ (considered as a groupoid) suggests hyperdoctrines that interpret each formula as an endofunctor(?) of $\mathrm{Set}$ (considered as a groupoid), which sounds like the type of thing that could feel new and interesting, though no specific instance springs to my own mind. | |
| Oct 4, 2021 at 21:41 | comment | added | So8res | Thanks! (And, I endorse your rephrasing of my question, and greatly appreciate your help in making it clear.) "Use a Boolean category other than Set" is much closer to an answer to my question. "Use $\mathrm{Set}^2$" is more concrete and therefore closer still. IIUC this is saying that some hyperdoctrines interpret formulas not as a set, but as a pair of sets (or, more generally, as an $X$-indexed set-family for $X$ an arbitrary groupoid)? And that's cool, but even cooler would be a specific interpretation of formulas of (say) PA as a pair of sets and which has intuitive pull in its own right. | |
| Oct 4, 2021 at 21:01 | history | answered | Mike Shulman | CC BY-SA 4.0 |