Timeline for What are some interesting hyperdoctrines that are not classical models?
Current License: CC BY-SA 4.0
21 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 4, 2021 at 14:59 | comment | added | So8res | Attempting to restate my Q in the wake of that miscommunication: The category of "hyperdoctrines for PA" (ie, the coslice category mentioned above), has an injection from the category of traditional models for PA (via powerset). This injection is not a surjection, as evidenced by the initial and terminal hyperdoctrines-for-PA. Hyperdoctrines-for-PA not in the image of that injection, can be thought of as "new model-like things" that make use of the fact that their lattices-of-interpretation needn't be powerset-lattices. I'm curious for example uses of that generality. | |
| Oct 4, 2021 at 14:50 | comment | added | So8res | I tried to make that explicit in my reply to @AlexKruckman's first clarifying question, above, which turned out to be astute. (Thanks, Alex!) Saying it in other words, just in case: The thing I'm calling the category of "hyperdoctrines for PA" is (equivalently) the coslice category (syntactic hyperdoctrine of PA $\downarrow$ Hyperdoctrine). And I sometimes say "a hyperdoctrine" to mean "a hyperdoctrine (for T)" when the theory T is clear from context, which I now see is confusing. Sorry for the confusion. Perhaps now that that's been cleared up, my question will make more sense :-p | |
| Oct 4, 2021 at 14:47 | comment | added | So8res | Ah, I think I might understand our miscommunication. I've been talking about "hyperdoctrines for PA", and this probably isn't standard notation. To be explicit, by "a hyperdoctrine for a theory T" I mean a hyperdoctrine additionally equipped with interpretations for each symbol in the language of T, and subject to the constraint that every axiom of T interprets to the top value in the algebra of interpretations for sentences. I agree that this can also be formalized as a hyperdoctrine equipped with a morphism to it from the syntactic hyperdoctrine of T. | |
| Oct 4, 2021 at 7:47 | comment | added | Zhen Lin | I feel you are being obtuse. I refer to the hyperdoctrine of [$\mathbb{N}$ as a set], the hyperdoctrine of [$\mathbb{N}$ as a monoid], the hyperdoctrine of [$\mathbb{N}$ as a model of PA], etc. They are different things, of course, but how are they different? Think carefully. Then consider that in the definition of hyperdoctrine, the bells and whistles required do not depend on the choice of language or theory, just the logical system. | |
| Oct 4, 2021 at 5:03 | comment | added | So8res | I don't know what you mean by "a hyperdoctrine of $\mathbb{N}$". I know how to think of $\mathbb{N}$ as a pure set, and I know how to think of $(\mathbb{N}, 0, \mathrm{succ}, ...)$ as a traditional model of PA, and I know how to think of $(\{n \mapsto \mathcal{P}(\mathbb{N}^n)\}, ...)$ as a hyperdoctrine for PA, and I know how to think of $(\mathbb{N}, 0, +)$ as a monoid. And by abuse of notation, it's fairly common to call all these $\mathbb{N}$, though of course this is just shorthand. But I'm not sure what a "hyperdoctrine of $\mathbb{N}$" is, or what examples you'd have me consider :-) | |
| Oct 4, 2021 at 5:00 | comment | added | So8res | I appreciate the bluntness (thanks!). I agree that the bracketing is ([a contravariant functor to BoolAlg], with bells and whistles) rather than (a contravariant functor to [BoolAlg with bells and whistles]). I'm not sure what I said that caused you to think I was bracketing the other way; apologies for the confusion. | |
| Oct 4, 2021 at 2:35 | comment | added | Zhen Lin | Let me be blunt. Your picture is wrong. A hyperdoctrine, in the first place, isn't a functor taking values in the category of [boolean algebras (or Heyting algebras or whatever) with bells and whistles] – the bracketing is wrong! A hyperdoctrine is a [functor taking values in the category of boolean algebras] with bells and whistles. You should go think carefully about some examples. What is the difference between the hyperdoctrine of $\mathbb{N}$ as a set and as a monoid and as a model of PA? | |
| Oct 4, 2021 at 0:56 | comment | added | So8res | And indeed, I'm not sure what you mean by hyperdoctrines "not being models" -- are you denying the obvious injection from traditional models to hyperdoctrines (using powerset)? b/c again, when I speak of a hyperdoctrine "being a model" I merely mean that it's in the image of that injection :-) | |
| Oct 4, 2021 at 0:56 | comment | added | So8res | I'm not sure what you mean by "hyperdoctrine equipped with a bunch of structure". In my picture, there are traditional models (which are sets equipped with some extra structure) and hyperdoctrines (which are contravariant functors to BoolAlg equipped with a bunch of structure), but I haven't myself been thinking in terms of hyperdoctrines equipped with additional structure. | |
| Oct 3, 2021 at 23:54 | comment | added | Zhen Lin | @So8res Your "hyperdoctrine equipped with a bunch of structure" can be most efficiently formulated as "hyperdoctrine equipped with a morphism from the syntactic hyperdoctrine". I think you haven't properly digested what I said about hyperdoctrines not being models. | |
| Oct 3, 2021 at 18:04 | comment | added | So8res | Like, we have an injection from the traditional models to the hyperdoctrines. We can think of any hyperdoctrine not in that image as a sort of "new model-like thing" that makes use of the fact that it can interpret formulas into something other than the powerset algebra. This is at least a little more general, as demonstrated by the initial and terminal hyperdoctrines. And intuitively, it should be much more general, b/c there should be lots of fun stuff you can do w/ non-powerset algebras, like using some topological or domain-theory inspired algebras instead. I'm quite curious for examples! | |
| Oct 3, 2021 at 17:45 | comment | added | So8res | (2) I don't think I understand your question. I'd say that the way you can distinguish $\mathbb{N}$-as-a-model-of-PA from $\mathbb{N}$-as-a-pure-set is that the former is a set plus some interpretations of the function/predicate symbols of PA, and the latter is just a set. And the way that you distinguish both of those from $\mathbb{N}$-as-a-hyperdoctrine-for-PA is that, when we encode it as a hyperdoctrine, we have a contravariant functor to BoolAlg equipped w/ a bunch of stucture. But probably I just don't understand what you're asking. | |
| Oct 3, 2021 at 17:41 | comment | added | So8res | (1) A contravariant functor from the category of natural numbers (w/ "substitution maps" in the obvious way, ie such that there are $m^n$ maps from $m$ to $n$) to BoolAlg, equipped with adjoints to substitution (quantifiers/equality) and subject to the usual constraints (Beck-Chevally, Frobenius reciprocity), plus interpretations of each n-ary predicate symbol as an object in the n'th BoolAlg, and such that every axiom of PA interprets (to an obj iso) to ⊤ in the 0th BoolAlg. Basically as described here. | |
| Oct 3, 2021 at 11:57 | comment | added | Alex Kruckman | @So8res Two clarifying questions: (1) What, precisely, is your definition of "hyperdoctrine for PA"? (2) Let's say we have a traditional model, say the standard model $\mathbb{N}$ for PA. Now you form the hyperdoctrine where the lattices are the powerset algebras of cartesian powers of $\mathbb{N}$. How does this construction encode the fact that we're thinking of $\mathbb{N}$ as a model of PA, not just as a pure set? | |
| Oct 2, 2021 at 17:49 | comment | added | So8res | And, I'm aware that the initial and terminal hyperdoctrines are "not traditional models" in this sense, and I'm sure that there are "uninteresting" ways to spawn more. But I continue to have the sense that there are "interesting" examples, that sound more like "there's a hyperdoctrine for PA where the boolean algebras are the decidable sets" or something, and that feel like they put the general powers of a hyperdoctrine (to use boolean algebras that aren't powerset algebras) to good use. Do you have any suggestions for what terminology I can use to zero in on that question? | |
| Oct 2, 2021 at 17:39 | comment | added | So8res | I'm sorry if I'm using non-standard terminology (this isn't my native field) :-) In my terminology, I'd say: every traditional model corresponds (via powerset) to a hyperdoctrine, in that if you give me a traditional model with universe $U$, I can give you a hyperdoctrine where the $n$th boolean algebra is the subsets of $U^n$. When I imply some hyperdoctrines are traditional models, I mean that some can be seen as "formed by powerset" in this sense. When I say I'm looking for a hyperdoctrine that does not correspond to a traditional model, I mean one that is not formed in this way. | |
| Oct 2, 2021 at 17:10 | comment | added | Alex Kruckman | @So8res Zhen Lin's point is that hyperdoctrines are not just not traditional models in general, they are not traditional models in any sense. That is, every hyperdoctrine is an example of a hyperdoctrine which is not a traditional model. Your question is like saying "I'm looking for concrete examples of theories in the language of groups which are not groups in the traditional sense." It's a type error. | |
| Oct 2, 2021 at 16:46 | comment | added | So8res | Yeah, I agree that hyperdoctrines are not (in general) traditional models, sorry for my confusing wording. In an answer, I'm looking for concrete examples of hyperdoctrines that aren't traditional models. Perhaps your example can be used to generate one (thanks!), though my current guess is that it's going to look more like the negative example in the penultimate paragraph of my original question, than the positive example. I'm still hoping for something more like "there's a hyperdoctrine for PA of only the decidable predicates", or something similarly specific and concrete. | |
| Oct 2, 2021 at 4:59 | comment | added | Zhen Lin | Hyperdoctrines are not models, as I wrote in the first paragraph. If you insist, a model is a morphism of hyperdoctrines – the domain being the theory being interpreted and the codomain being the universe of interpretation. "Interesting" is in the eye of the beholder. For example, you could take the syntactic hyperdoctrine of the first order theory of an infinite structure over a countable signature, then regard it as a model of some subtheory. This will be a non-classical model because its lattices are countably infinite. | |
| Oct 2, 2021 at 1:47 | comment | added | So8res | I buy that this construction works (thanks!), but insofar as you're trying to argue that all hyperdoctrines are "non-interesting" (in the sense of the question), I don't yet see the argument. The sort of thing I'm looking for is more like "there's a hyperdoctrine where the nth lattices is only the computable properties of n numbers" or something (I don't think that's true as stated). While I agree all hyperdoctrines admit your construction here, I don't know how to use it to produce a specific "new" hyperdoctrinal model, nor how to see it as essentially ruling all interesting ones out. | |
| Oct 2, 2021 at 0:46 | history | answered | Zhen Lin | CC BY-SA 4.0 |