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
  Isabelle/ZF - Lawrence Paulson (University of Cambridge)
DTSTART:20080610T120000Z
DTEND:20080610T130000Z
UID:TALK11661@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:The proof of the relative consistency of the axiom of choice h
 as been mechanized using Isabelle/ZF. The proof builds upon a previous mec
 hanization of the reflection theorem. The heavy reliance on metatheory in 
 the original proof makes the formalization unusually long\, and not entire
 ly satisfactory: two parts of the proof do not fit  \ntogether. It seems i
 mpossible to solve these problems without formalizing the metatheory. Howe
 ver\, the present development follows a standard textbook\, Kunen's Set Th
 eory\, and could support the formalization of further material from that b
 ook. It also serves as an example of what to expect when deep mathematics 
 is formalized.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR