The constructions and proofs of this paper are to be understood as taking place in some kind of basic set theory or type theory, based on intuitionistic logic. \lie assunie a set N of natural numbers, satisfying HEYTING'S arithmetic (with full induction) ; we can form products of sets, and subsets of them, by comprehension. We may quantify over all subsets of a set, but the power-set of set is only needed in 2.6 and 3.5. 0.1. E q u a l i t i e s . An equality on a set A is a reflexive, transitive, symmetric binary relation, usually denoted z A , or just z .
in the presence of an equality, all subsets referred to are supposed (unless otherwise indicated) to be extensional. The standard equality on a set is just the identity relation =.
If z is an equality on A , we write, for a
The point of allowing the structures of SS 1 -3 to have (non-standard) equalities on them, instead of always taking quotients? is that this permits a distinction between functions and operations on such sets (see subsection following); we will need this for the proof that โฌI.-\ RTOGS' numbers of infinite sets are regular well-ordering*, \i-it.liout using the Axiom of Choice.