Quotients, pure existential completions and arithmetic universes

TL;DR

This paper characterizes Joyal's arithmetic universes via the exact and regular completions of pure existential completions, linking them to doctrines of predicates and providing a new perspective on their structure.

Contribution

It introduces a novel characterization of arithmetic universes as exact completions of pure existential completions of predicate doctrines, generalizing previous results.

Findings

Arithmetic universes are the exact completions of pure existential completions.

The initial arithmetic universe in ZFC-sets is the completion with exact quotients of recursively enumerable predicates.

The results unify and extend previous characterizations of arithmetic universes.

Abstract

We provide a new description of Joyal's arithmetic universes through a characterization of the exact and regular completions of pure existential completions. We show that the regular and exact completions of the pure existential completion of an elementary doctrine $P$ are equivalent to the $\mathsf{reg}/\mathsf{lex}$ and $\mathsf{ex}/\mathsf{lex}$-completions, respectively, of the category of predicates of $P$. This result generalizes a previous one by the first author with F. Pasquali and G. Rosolini about doctrines equipped with Hilbert's $\epsilon$-operators. Thanks to this characterization, each arithmetic universe in the sense of Joyal can be seen as the exact completion of the pure existential completion of the doctrine of predicates of its Skolem theory. In particular, the initial arithmetic universe in the standard category of ZFC-sets turns out to be the completion with exact quotients of the doctrine of recursively enumerable predicates.