BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Isaac Newton Institute Seminar Series
SUMMARY:The relative consistency of the axiom of choice me
chanized using Isabelle/ZF - Paulson\, L (Universi
ty of Cambridge)
DTSTART;TZID=Europe/London:20120322T133000
DTEND;TZID=Europe/London:20120322T150000
UID:TALK37089AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/37089
DESCRIPTION:The proof of the relative consistency of the axiom
of choice has been mechanized using Isabelle/ZF\,
building on a previous mechanization of the refle
ction theorem. The heavy reliance on metatheory in
the original proof makes the formalization unusua
lly long\, and not entirely\nsatisfactory: two par
ts of the proof do not fit together. It seems impo
ssible to solve these problems without formalizing
the metatheory. \nHowever\, the present developme
nt follows a standard textbook\, Kenneth Kunen's S
et theory: an introduction to independence proofs\
, and could support the formalization of further m
aterial from that book. It also serves as an examp
le of what to expect when deep mathematics is form
alized.\n\n
LOCATION:Discussion Room\, Newton Institute
CONTACT:Mustapha Amrani
END:VEVENT
END:VCALENDAR