Output details

An induction principle for consequence in arithmetic universes

<11>For the first time gives evidence to a 1999 conjecture that Joyal's arithmetic universes might have some ability to stand in for Grothendieck toposes as classifiers for geometric theories and hence as generalized spaces. This arises out of questions, motivated by computer science, of finitariness for geometric logic in point-free topology.

For the first time analyses the structure of certain kinds of "subspaces" of general arithmetic universes, showing the relation with sheaf theory. Novel applications, including a novel induction principle, show techniques for dealing with the fact that arithmetic universes are not in general cartesian closed.