Stanford Encyclopedia of Philosophy

Supplement to Set Theory: Constructive and Intuitionistic ZF

Set-theoretic principles incompatible with intuitionistic logic

In this supplementary document we show how two well-known set-theoretic principles, foundation and choice, are incompatible with set theories based on intuitionistic logic: the assumption of either of these principles implies instances of the constructively unacceptable principle of the excluded middle (EM). (See also the discussion on these principles in the main document: Constructive and intuitionistic ZF.) We also briefly discuss another principle (linearity of ordinals) that gives rise to exlcuded middle. For the sake of readabiliy, we use lower and upper case letters to denote sets.

Foundation implies instances of EM

The axiom of foundation (or regularity) states that every inhabited (non-empty) set has an ∈-minimal element. Formally:

∀x[∃y ∈ x → ∃y(y ∈ x ∧ ∀z(z ∈ y → ¬(z ∈ x)))].

We here show that instances of the excluded middle can be derived from foundation on the basis of some minimal set-theoretic assumptions. In fact, the following argument can be carried out on the basis of a subsystem of CZF including bounded separation, emptyset, and the axiom of pair. We can thus form the set {0,1} of the von Neumann natural numbers 0 and 1, where 0 is the empty set and 1 is the singleton containing the empty set only.

Let ψ be a bounded formula and assume foundation. By bounded separation, let

A := {y ∈ {0,1}: y = 1 ∨ (y = 0 ∧ ψ)}.

We can now easily derive the excluded middle for ψ. As 1 ∈ A, the set A is inhabited. By foundation there exists a minimal element Y ∈ A, that is, Y is such that for all Z ∈ Y, Z does not belong to A. Since Y is an element of A, we have either Y = 1 or Y = 0 ∧ ψ.

In either case, we have ψ ∨ ¬ ψ. This argument shows that we can intuitionstically prove excluded middle for bounded sentences if we assume foundation. In systems with full (i.e. unbounded) separation, as IZF, the same argument can be used to show that EM is derivable from foundation.

The axiom of choice implies instances of EM

We here show that the axiom of choice (AC) implies instances of the excluded middle within a basic constructive set theory. Therefore we can not assume AC in a set theory based on intuitionistic logic. We recall that some consequences of AC, like countable choice, are instead compatible with constructive and intuitionistic ZF (see also the main document section on Constructive Choice Principles).

The following argument can be carried out, for example, on the basis of a subtheory of CZF that includes extensionality, pair, union, empty set, infinity, bounded separation, replacement and bounded induction on the natural numbers. (Such a system essentially coincides with Aczel and Rathjen's Elementary Constructive Set Theory, ECST, in Aczel and Rathjen 2001). Note that extensionality and separation play an essential role in the following proof.

By AC we denote the principle:

∀u∀v[(∀x ∈ u)(∃y ∈ v) ψ(x,y) → (∃f: u → v)(∀x ∈ u) ψ(x,f(x))],

where “F: U → V” stands for a formula expressing the fact that F is a set theoretic function with domain U and range included in V. The notions of set theoretic function, domain and range can be formalised in a standard way in constructive set theory (see, e.g., Aczel and Rathjen 2001).

Let φ be a bounded formula and define the following sets (by bounded separation):

We note that (∀z ∈ {A,B})(∃n ∈ {0,1})(n ∈ z).

By AC, let F: {A,B} → {0,1} be a choice function with F(A) ∈ A and F(B) ∈ B. Here we need to use a crucial fact about the natural numbers. As the values of F are natural numbers we can prove (by a bounded form of induction on the natural numbers) that either F(A) = F(B) or F(A) ≠ F(B). Now we argue as follows.

In either case, we have proved φ∨¬φ.

Also in this case, the same argument can be used to show that EM follows from AC in a system with full separation instead of bounded separation.

Constructive ordinals

Arguments analogous to those just presented can be used to show that standard classical properties of the ordinals, such as the linearity of their order, imply instances of EM.

There are various classically equivalent definitions of ordinal number. In a constructive context, ordinals are usually defined as hereditarily transitive sets (following Powell 1975). A set is transitive if its elements are subsets of it. That is, U is transitive if ∀X ∈ U (X ⊆ U), that is, ∀X ∈ U ∀Z ∈ X (Z ∈ U). A ordinal is then defined as a transitive set all of whose elements are also transitive. The order on the ordinals is given by the membership relation. Linearity of an ordinal α is the property: ∀β ∈ α∀γ ∈ α (β ∈ γ ∨ β = γ ∨ γ ∈ β). It is an easy exercise to prove (using arguments analogous to those above) that assuming linearity for all ordinals yields instances of the excluded middle.

This example shows that in constructive set theory the notion of ordinal does not play the same central role as in classical set theory. However, ordinals supply us with a ranking of the universe and we can still define many of the familiar set-theoretic operations by transfinite recursion on ordinals (see Aczel and Rathjen 2001, Section 4.2). This is fine as long as the definitions by transfinite recursion do not make case distinctions such as in the classical ordinal cases of successor and limit.

Bibliographic information for this supplementary document is in the Bibliography for this entry.