Constructive Set Theory

I’m reading chapter 3, entitled “Set Theory” of Constructive Analysis by Errett Bishop and Douglas Bridges. It’s pretty hard to figure out what the author means. For instance:

… a set is defined by describing what must be done to construct an element of the set, and what must be done to show that two elements of the set are equal.

The author defines a subset A of a set B to be a set A along with a suitable inclusion map i:A ⇒ B. Anyhow, to give an idea how vague his definition of a set is, consider the following definition of the void subset (∅) of any set S.

The void subset ∅ of a set S is defined as follows. To construct an element x of ∅, construct an element s of S and prove that 0=1; the inclusion map is defined by i(x)≡s. The definition of ∅ is negativistic, and we prefer to mention the void set as seldom as possible.

Firstly, there might not be a way of constructing an element s of S. Secondly, how is one supposed to prove that 0=1?

Fortunately I know type theory, and know what he is trying to say. His definition of a set is what is ‘commonly’ known as a setoid. A setoid is a type, and an equivalence relation. More accurately it is a triple <S, ≈_S, p_S, ≈S>. where:

1. S is a type.
2. ≈_S is a function from S×S producing a type.
3. p_S, ≈S is a proof that ≈_S is an equivalence relation.

Really p is also a triple of three proofs. One proving reflexivity, one proving symmetry, and one proving transitivity. You can divide the structures up however you want.

Anyhow a subset of a set <S, ≈_S, p> would be a set <A, ≈_A, q> and an inclusion map i:A ⇒ S, and a proof r that whenever a≈_Aa′ then i(a)≈_Si(a′).

Finally we can defined the void subset of a set <S, ≈_S, p> as having the type ⊥ (bottom), with = (Leibniz’s equality, but really any function will do). The inclusion map will be abort_S:⊥ ⇒ S. Finally, to prove the inclusion map is sound:

1. We are given a:⊥ and a′:⊥ and that a=a′.
2. a:⊥ is impossible, so by contradiction we are done (in otherwords return abort_{abortS(a)≈SabortS(a′)}(a)).

(If you want, you can take ⊥≡(0=1), as there is a canonical bijection between the two types.)

See, wasn’t that more clear? I’m not really sure that the definition is negativistic. Negativistic things are of the form foo ⇒ ⊥, but our inclusion map is the other way: ⊥ ⇒ foo. I think the author may be in error on this point.