Abstract

We analyze Zorn's Lemma and some of its consequences for Boolean algebras in a constructive setting. We show that Zorn's Lemma is persistent in the sense that, if it holds in the underlying set theory, in a properly stated form it continues to hold in all intuitionistic type theories of a certain natural kind. We also establish the persistence of some familiar results in the theory of Boolean algebras--notably, the proposition that every complete Boolean algebra is an absolute subretract. This resolves a question of Banaschewski and Bhutani as to whether the Sikorski extension theorem for Boolean algebras is persistent.