Jon Zappe

Kripke's schema is a fragment of the law of excluded middle that captures the essence of Brouwer's creating subject. The two versions in which Kripke's schema usually occurs differ from each other by an instance of countable choice. We introduce Kripke's schema to constructive reverse mathematics by using either version as a point of reference for some classifications. The weaker version (respectively, the stronger version) of Kripke's schema is equivalent to statements of the following kind: every subset of a finitely enumerable set (respectively, of a countable set) is countable; the intersection of two finitely enumerable sets (respectively, of two countable sets) is countable; etc. To see this requires to consider a variant of the notion of countability that includes the empty set, and to work in a setting as innocent as constructive Zermelo-Fraenkel set theory, which none of the principles under scrutiny is part of.