Forcing for Constructive Set Theory
Florida Atlantic University
As is well known, forcing is the same as Boolean-valued models. If instead of a Boolean algebra one used a Heyting algebra, the result is a Heyting-valued model. The result then typically models only constructive logic and falsifies Excluded Middle. On the one hand, many of the same intuitions from forcing carry over, while on the other the result is quite foreign to a classical mathematician. I will give a survey of perhaps too many examples, and call for the importation of more methods from current classical set-theory into constructivism.
Robert Lubarsky got his PhD in mathematics in 1984 from MIT. He currently holds a position at Florida Atlantic University, and his research interests lie in the areas of constructive mathematics, higher computability theory and set theory.