S, a first-order theory, is two-sorted because its ontology includes "stages" as well as sets.
Any grouping together of mathematical, abstract, or concrete objects, however formed, is a collection, a synonym for what other set theories refer to as a class.
A common instance of a collection is the domain of discourse of a first-order theory.
The iterative conception has gradually become more accepted, despite an imperfect understanding of its historical origins.
The iterative conception of set steers clear, in a well-motivated way, of the well-known paradoxes of Russell, Burali-Forti, and Cantor.
These paradoxes all result from the unrestricted use of the principle of comprehension of naive set theory.
Identity, denoted by infix '=', does not play the role in S it plays in other set theories, and Boolos does not make fully explicit whether the background logic includes identity.
[3] The symbolic axioms shown below are from Boolos (1998: 91), and govern how sets and stages behave and interact.
The natural language versions of the axioms are intended to aid the intuition.
The first group consists of axioms pertaining solely to stages and the stage-stage relation ‘<’.
The sole purpose of Inf is to enable deriving in S the axiom of infinity of other set theories.
The second and final group of axioms involve both sets and stages, and the predicates other than '<': All:
The role of Spec in S is analogous to that of the axiom schema of specification of Z. Boolos’s name for Zermelo set theory minus extensionality was Z-.
[4] The purpose of this exercise was to show how most of conventional set theory can be derived from the iterative conception of set, assumed embodied in S. Extensionality does not follow from the iterative conception, and so is not a theorem of S. However, S + Extensionality is free of contradiction if S is free of contradiction.
Boolos then altered Spec to obtain a variant of S he called S+, such that the axiom schema of replacement is derivable in S+ + Extensionality.
[5] Hence S+ + Extensionality cannot prove those theorems of the conventional set theory ZFC whose proofs require Choice.