Prof. P. Johnstone will give a lecture on Friday 23 at 11:00 in Sala del Consiglio, at the Department of Mathematics and Computer Science.
“Toposes as higher-order theories”
Abstract. The elementary reformulation of topos theory by Lawvere and Tierney allowed scope for the interpretation not only of first-order but also of higher-order logic; in particular, it allows one to construct a topos which is the “embodiment” of an arbitrary higher-order theory.
Of particular interest is the so-called “free topos”, which embodies the empty theory (the theory with no axioms): the internal structure of this topos directly reflects the proof theory of higher-order intuitionistic type theory. What is of particular interest is that, although the free topos is a highly “exotic” and mysterious entity, remarkably simple proofs of intuitionistic principles such as the existence and disjunction properties, Markov’s principle and Brouwer’s Continuity Theorem can be given by studying its interaction with familiar Grothendieck toposes. The lecture will also include Freyd’s proof that the axiom of infinity is conservative relative to higher-order intuitionistic type theory.
