Mathematical logic seminar - November 3 2009

Time: 12:00 - 13:20

Room: Doherty Hall 4303

Speaker:     Peter Lumsdaine   
CMU

Title: Fixed-point theorems, constructively

Abstract:

The Bourbaki-Witt and Tarski fixed-point theorems for chain-complete posets are two minor gems of early set theory: simple and natural statements about posets, easily and elegantly proven with transfinite induction.

In constructive logic, the situation is less simple. I will sketch a counterexample (in the effective topos, a realisability model) showing that neither can be proven entirely constructively; and I will show how they are in fact equivalent to the existence of enough ordinals.