BEGIN:VCALENDAR VERSION:2.0 PRODID:ILLC Website X-WR-TIMEZONE:Europe/Amsterdam BEGIN:VTIMEZONE TZID:Europe/Amsterdam X-LIC-LOCATION:Europe/Amsterdam BEGIN:DAYLIGHT TZOFFSETFROM:+0100 TZOFFSETTO:+0200 TZNAME:CEST DTSTART:19700329T020000 RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU END:DAYLIGHT BEGIN:STANDARD TZOFFSETFROM:+0200 TZOFFSETTO:+0100 TZNAME:CET DTSTART:19701025T030000 RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU END:STANDARD END:VTIMEZONE BEGIN:VEVENT UID:/NewsandEvents/Archives/2002/newsitem/239/20-J une-2002-What-is-the-world-of-mathematics-Joachim- Lambek DTSTAMP:20020613T000000 SUMMARY:What is the world of mathematics?, Joachim Lambek ATTENDEE;ROLE=Speaker:Joachim Lambek DTSTART;TZID=Europe/Amsterdam:20020620T140000 DTEND;TZID=Europe/Amsterdam:20020620T150000 LOCATION:De Uithof, Centrum-Gebouw Zuid, Room F119 , Utrecht DESCRIPTION:Abstract: It may be argued that the language of mathematics is {\\it about the} catego ry of sets, although the definite article requires some justification. As possible worlds of mathema tics we may admit all models of type theory, by wh ich we mean all {\\it local toposes}. For an intui tionist, there is a distinguished local topos, nam ely the so-called {\\it free topos}, which may be constructed as the Tarski-Lindenbaum category of i ntuitionistic type theory. However, for a classica l mathematician, to pick a distinguished model may be as difficult as to define the notion of truth in classical type theory, which Tarski has shown t o be impossible. This event is coordinated with the Sixth Workshop on Games in Logic, Language an d Computation, which will take place at the same l ocation on the same date. For more information, se e http://www.illc.uva.nl/~bcate/gllc6/ . X-ALT-DESC;FMTTYPE=text/html:\n
\n
Abstract:
\n It may be argued that the l
anguage of mathematics is {\\it about the}\ncatego
ry of sets, although the definite article requires
some justification. As\npossible worlds of mathem
atics we may admit all models of type theory, by w
hich\nwe mean all {\\it local toposes}. For an int
uitionist, there is a distinguished\nlocal topos,
namely the so-called {\\it free topos}, which may
be constructed as\nthe Tarski-Lindenbaum category
of intuitionistic type theory. However, for a\ncla
ssical mathematician, to pick a distinguished mode
l may be as difficult as to\ndefine the notion of
truth in classical type theory, which Tarski has s
hown to\nbe impossible.\n