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: Iterated Hyperdoctrine

Fawzi Hreiki (Sep 28 2020 at 11:17):

The usual slogan is that basic propositional logic is the internal language of certain kinds of posets - of course, this isn't the whole truth but it's a good starting point. Then, first-order logic is the internal language of first-order hyperdoctrines, which are cartesian closed categories $T$ equipped with a functor $P: T^{op} \rightarrow L$ where $L$ is an appropriate 2-category of posets and where each $P(f): P(Y) \rightarrow P(X)$ has left and right adjoints expressing existential and universal quantification respectively. Usually we also need this functor to satisfy some other conditions (Beck-Chevalley, Frobenius reciprocity) to make sure that everything runs as expected. My question is if anyone has tried to iterate this process, or if such a thing would work at all. That is, can we define a second-order hyperdoctrine to be a cartesian closed category $T$ with a functor $P: T^{op} \rightarrow L$ where $L$ is a 2-category of first-order hyperdoctrines, and so on for all $n$ ?

Nathanael Arkor (Sep 28 2020 at 12:13):

I've thought about the same question, and I believe some construction along these lines should work, though the compatibility conditions may be quite subtle and would require some thought. I looked around for such a construction in the literature a while ago, and couldn't find anything, but it's possible I overlooked something. One thing to be aware of is that "order" (e.g. "second-order" and "higher-order") in logic/type theory is so overloaded that "second-order hyperdoctrine" could mean any number of things, so it's best to be aware of that when searching for this terminology.

Nathanael Arkor (Sep 28 2020 at 12:13):

I believe this would be "order" in the sense that some call the polymorphic $\lambda$-calculus "second-order $\lambda$-calculus".

Fawzi Hreiki (Sep 28 2020 at 19:40):

I'll have a think about it but I don't imagine it should be too difficult to go up to $n$ for any natural number $n$. What I'd really like to know is if we can define the notion of a higher-order hyperdoctrine (perhaps by taking the directed colimit over all the $n$) and using that to model higher-order type theory, with toposes as special cases (where the hyperdoctrine structure is given by slicing).

Fawzi Hreiki (Sep 28 2020 at 19:41):

Also, you're probably right about the overloading of terminology, but '$n$-th order logic' is quite well established and I don't really know what else it could be called anyway.

Reid Barton (Sep 28 2020 at 19:50):

For a first-order hyperdoctrine, shouldn't $T$ be not cartesian closed but just a category with finite products? Otherwise, you have something higher-order going on already.

Dan Doel (Sep 28 2020 at 19:50):

It seems like the issue might be that the 'second order' part in iterating hyperdoctrines isn't the same as normal second order quantification (which I think is what Nathanael was saying). You might be able to quantify over proposition variables but not predicates. However, I haven't thought hard enough to actually be sure.

Dan Doel (Sep 28 2020 at 19:59):

I guess it's not like that, because $P$ has predicates of all arities? The propositions are the image of $1$?

Nathanael Arkor (Sep 28 2020 at 20:14):

From a type theoretic perspective (which is the angle I had been coming from), iterating this construction corresponds to quantifying over kinds, kinds of kinds, etc. Usually, instead of consider kinds of kinds of (etc.), one starts to consider universes instead (which are related, but formalised differently).

Nathanael Arkor (Sep 28 2020 at 20:15):

Whereas the usual "higher-order" structure in a hyperdoctrine would come from cartesian-closure, as Reid points out.

Fawzi Hreiki (Sep 28 2020 at 20:19):

No, because the 'order' comes not from the exponentials, but from the quantifiers. The exponential in a poset can be construed as the (internal) implication connective which reflects the (external) entailment relation. A Heyting algebra, for example, is cartesian closed, but it only gives us propositional logic.

Nathanael Arkor (Sep 28 2020 at 20:20):

There's a notion of hyperdoctrine that already gives rise to toposes, called a tripos. So higher-order logic can already be interpreted in this "first-order" setting.

Dan Doel (Sep 28 2020 at 20:22):

$T$ being Cartesian closed means the universe of discourse has exponentials, not the propositions.

Fawzi Hreiki (Sep 28 2020 at 20:36):

I think that $T$ being cartesian closed gives the 'physical universe' higher-order constructions, but the 'internal discourse' is given by the functor $P$ which assigns to each object $X \in T$ its own 'mini universe of discourse' $P(X)$. We need to be careful to distinguish between the internal logic of a category (or system of categories) and what we can say about that category in our metatheory, whatever that happens to be. So if $P(X)$ is a poset for each object $X$, we only get one layer of quantification and so $P$ only provides us with first-order logic internally.

Fawzi Hreiki (Sep 28 2020 at 20:40):

I'll read into triposes (tripoi?). Thanks

Dan Doel (Sep 28 2020 at 23:04):

I guess another thing I didn't mention is: it's not clear to me that what you get by iterating isn't like "Henkin semantics." That is essentially a first-order semantics of second-order logic, where the values of the second-order quantifiers are given (relatively) arbitrary interpretations. In such a case, it's subject to the same 'not really second order' objection.

Dan Doel (Sep 28 2020 at 23:09):

For 'real' second-order stuff, you might not need another layer of categories, but some kind of completeness on $L$ with respect to $T$. I'm not really sure.

Fawzi Hreiki (Sep 29 2020 at 10:53):

I don’t know too much about second-order semantics but isn’t it the case that the standard semantics allows full second-order quantification (ie over all first-order predicates) whereas the Henkin semantics is what restricts second-order quantification?

Dan Doel (Sep 29 2020 at 14:42):

The syntax is identical. The difference is in the models. 'Standard' semantics says that the second order quantifiers are valued in the 'actual' subsets of whatever the first-order quantified in. Henkin semantics just allows another choice of set to model the second-order quantifiers. If anything, standard semantics are more 'restrictive'.