# Prof Philip Scott - Free Topos Seminar

Laboratory for Foundations of Computer Science (LFCS),

University of Edinburgh presents:

***** What is the free topos? *****

by Philip Scott, Dept. of Mathematics and Statistics, University of Ottawa

SICSA Distinguished Visiting Fellow

More information available at: __http://wcms.inf.ed.ac.uk/lfcs/events/prof.-phil-scott-free-topos-lecture__

Abstract:

The free topos is a model of intutionistic higher order logic, and may be thought of as a universe of sets for a moderate intuitionist. In this lecture, we give an introduction to free topoi (on graphs); in particular, we discuss metamathematical properties of the free topos (generated by the empty graph), which is an initial object in the category of all toposes with logical functors.

The free topos satisfies many interesting properties corresponding to proof-theoretic principles of intuitionistic higher-order logic, and indeed allows us to reprove these properties in an elegant algebraic way. This includes such familiar properties as the existence and disjunction properties, uniformity principles, independence of

premisses, as well as various choice principles. We shall discuss uniform categorical proofs, based on gluing methods of Peter Freyd, as well as connections with realizability. If time permits, we discuss more recent results.

Video