Personal tools
You are here: Home Events Prof. Phil Scott, Free topos lecture

Prof. Phil Scott, Free topos lecture

What
When Jul 13, 2011
from 02:00 PM to 05:00 PM
Where IF 4.31+4.33, Informatics Forum
Contact Name
Add event to calendar vCal
iCal

 Laboratory for Foundations of Computer Science (LFCS) presents:

 

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

 

An afternoon of lectures by Philip Scott , Dept. of Mathematics and Statistics, University of Ottawa
SICSA  Distinguished Visiting Scholar

Location: Informatics Forum, Room 4.31/33, School of Informatics, University of Edinburgh, Scotland. Map.
Time: 14:00-17:00, 13 July 2011.


Abstract:  

The free topos is a model of intuitionistic 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.

 

Coffee and refreshments will be served from 13:00-14:00 in Mini-Forum 2 on the fourth floor. We also plan to go for a meal after the lectures


If you intend to come, it would be helpful (but not essential) to send
us a short email saying so.  If you want to come to dinner afterwards, please tell us by Monday 11 July.

 

For RSVP and any questions
Contact: b.i.kavanagh@sms.ed.ac.uk

 

Schedule: 

1300-1400 :  Coffee

14:00-15:30: Lecture

15:30--15:40: Short Break

15:40-17:00: Lecture

17:30-18:30: Meet at Pub (location TBD)

18:45- :  Dinner (location TBD)

 

Background Reading:

For graduate students who would like to prepare for the lectures Phil  will cover Part 2, sections 20--21, and sections 11-14 of his book with Lambek, "Introduction to higher order categorical logic", which provides excellent exercises.

 

p.p1 {margin: 0.0px 0.0px 0.0px 0.0px; font: 16.0px Courier}

Document Actions