Timeline for What are some interesting hyperdoctrines that are not classical models?
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 4, 2021 at 17:06 | comment | added | So8res | Like, hyperdoctrines are cool, and this whole idea of putting models and interpretations on the same footing is cool, and it feels to me like I should be able to go back to the 1920s and tell Skolem about this cool and more general tool for doing semantics. And he could rightly ask "if this is so cool, what interpretations do you have that I don't?". And I could say "I can interpret PA using the syntax of PA, or of PA + Con(PA), or of ZFC, using exactly the same machinery I use to interpret PA using the nats". And that is indeed cool! But are there any other new interpretations I can show off? | |
| Oct 4, 2021 at 16:59 | comment | added | So8res | With regards to a hyperdoctrine-for-PA of decidable predicates, I'm aware this doesn't work as stated (I tried it before asking my Q :-p), but I don't see your argument as working against plausible repairs thereof. Like, is there a hyperdoctrine-for-PA where the nth BoolAlg is the decidable predicates (on n numbers) with an extra "undecidable" point adjoined? Probably not (I looked briefly at that too), but I'm still holding out for there being some sort of cool computational / topological / domain-theoretic / ??? thing you can do w/ hyperdoctrines that you can't do with models. | |
| Oct 4, 2021 at 16:58 | comment | added | So8res | Thanks! $H(\text{ZFC})$ is a lot closer to the sort of concrete example I'm looking for. And while I buy the argument that every hyperdoctrine is "syntactic" for some (not necessarily enumerable) theory, I'm still interested in hyperdoctrines for PA that aren't enumerable, and that in a sense "feel like" they're taking advantage of the hyperdoctrine-ability to interpret formulas using non-powerset algebras, in some manner other than "quotient sentences by provability in some enumerable extension of PA". | |
| Oct 4, 2021 at 16:50 | comment | added | Alex Kruckman | @მამუკაჯიბლაძე Should be, since all formulas are generated (under the logical connectives) by the symbols in the language, which are decidable. But note also that we're talking about hyperdoctrines admitting a morphism from the syntactic hyperdoctrine of PA. There's no reason a sub-hyperdoctrine should admit such a morphism, unless it is the whole syntactic hyperdoctrine. | |
| Oct 4, 2021 at 16:46 | comment | added | მამუკა ჯიბლაძე | So, is the sub-hyperdoctrine of $H(\textsf{PA})$ generated by decidable predicates (if such thing exists) the whole of $H(\textsf{PA})$? | |
| Oct 4, 2021 at 15:49 | history | edited | Alex Kruckman | CC BY-SA 4.0 |
added 6 characters in body
|
| Oct 4, 2021 at 15:43 | history | answered | Alex Kruckman | CC BY-SA 4.0 |