 As to the first step, consisting in eliminating the principle of excluded middle from the logic, it turns out that simply evicting this principle from the underlying logic is insufficient; that is, it is not enough to take the intuitionistic rather than the classical predicate calculus as our basis. We also need to ensure that the set theoretic axioms do not bring undesirable forms of excluded middle back into our theory. For example, as noted by Myhill (1973), we need extra care in choosing an appropriate statement for the axiom of foundation. Foundation is introduced in set theory to rule out sets which are members of themselves and thus \(\in\)-chains of sets. The usual formulation of foundation asserts that each inhabited set (a set with at least one element) has a least element with respect to the membership relation. This statement, however, can be shown to yield constructively unacceptable instances of excluded middle on the basis of modest set-theoretic assumptions. Therefore the usual formulation of foundation has to be omitted from a set theory based on intuitionistic logic. For a proof, see the supplementary document: