BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The relative consistency of the axiom of choice mechanized using I
 sabelle/ZF - Paulson\, L (University of Cambridge)
DTSTART:20120322T133000Z
DTEND:20120322T150000Z
UID:TALK37089@talks.cam.ac.uk
CONTACT:Mustapha Amrani
DESCRIPTION:The proof of the relative consistency of the axiom of choice h
 as been mechanized using Isabelle/ZF\, building on a previous mechanizatio
 n of the reflection theorem. The heavy reliance on metatheory in the origi
 nal proof makes the formalization unusually long\, and not entirely\nsatis
 factory: two parts of the proof do not fit together. It seems impossible t
 o solve these problems without formalizing the metatheory. \nHowever\, the
  present development follows a standard textbook\, Kenneth Kunen's Set the
 ory: an introduction to independence proofs\, and could support the formal
 ization of further material from that book. It also serves as an example o
 f what to expect when deep mathematics is formalized.\n\n
LOCATION:Discussion Room\, Newton Institute
END:VEVENT
END:VCALENDAR