From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6735 Path: news.gmane.org!not-for-mail From: Benedict Kavanagh Newsgroups: gmane.science.mathematics.categories Subject: LFCS Free Topos Seminar, Phil Scott, 13 July, Edinburgh, Scotland Date: Mon, 4 Jul 2011 12:21:22 +0100 Message-ID: Reply-To: Benedict Kavanagh NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Trace: dough.gmane.org 1309782636 31375 80.91.229.12 (4 Jul 2011 12:30:36 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Mon, 4 Jul 2011 12:30:36 +0000 (UTC) To: categories@mta.ca Original-X-From: majordomo@mlist.mta.ca Mon Jul 04 14:30:32 2011 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtpx.mta.ca ([138.73.1.30]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1QdiII-0004Jd-2x for gsmc-categories@m.gmane.org; Mon, 04 Jul 2011 14:30:30 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:45929) by smtpx.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1QdiGT-0006ki-0P; Mon, 04 Jul 2011 09:28:37 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1QdiGS-0001Rq-9n for categories-list@mlist.mta.ca; Mon, 04 Jul 2011 09:28:36 -0300 Original-Content-Transfer-Encoding: quoted-printable Content-Disposition: inline Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6735 Archived-At: If you will be in Scotland on July 13 please consider attending an afternoo= n of lectures on the free topos by Philip Scott. You will find the announcement = below. -Ben ---------------------------------------------------------------------------= --- Laboratory for Foundations of Computer Science (LFCS),=20 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 Location: Informatics Forum, Room 4.31/33, School of Informatics, Universit= y of Edinburgh, Scotland. Time: 14:00-17:00, 13 July 2011. 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. ----------------------- [For admin and other information see: http://www.mta.ca/~cat-dist/ ]