Toposes as higher-order theories
speaker: Peter Johnstone (University of Cambridge)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.
timetable:
Tue 20 Apr, 14:30 - 16:30, Sala dei Seminari
<< Go back