BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Almost always blue trees and bar induction - Tarmo Uustalu\, Talli
 nn University of Technology
DTSTART:20111028T130000Z
DTEND:20111028T140000Z
UID:TALK33661@talks.cam.ac.uk
CONTACT:Bjarki Holm
DESCRIPTION:Let us do constructive temporal logic on infinite binary trees
  whose nodes are colored red or blue. It turns out that there are more pos
 itive notions of an almost always blue tree than one might first think and
  that the relationships between these are subtle.\n\nWe organize five almo
 st always blueness predicates into a\npentagon-shaped diagram. Along the f
 ive arcs\, the predicates entail each other intuitionistically. Four of ou
 t of the five converse implications hold under specific assumptions: the f
 an theorem (FAN)\, bar induction (BI)\, the lesser principle of omniscienc
 e (LPO) and weak continuity for numbers (WCN)\; the fifth is contradictory
 . On a very simple example tree\, one of the predicates is undecided intui
 tionistically\, but true resp. false in two consistent but mutually contra
 dictory extensions (LPO and WCN).\n\n(Joint work with Marc Bezem\, Keiko N
 akata.)
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR