Page 67 - Textos de Matemática Vol. 38

ORDINALS, COMPUTATIONS, AND MODELS OF SET THEORY 59
7. Surjectivity of pairing (SUR): ∀α∃β, γ(α = g(β, γ));
8. Axiom schema of separation (SEP): For all LSO-formulae φ(α,P1,...,Pn) postulate:
∀P1, . . . , Pn∀a∃b∀α(α ∈ b ↔ α ∈ a ∧ φ(α, P1, . . . , Pn));
9. Axiomschemaofreplacement(REP):ForallLSO-formulaeφ(α,β,P1,...,Pn) postulate:
∀P1,...,Pn(∀ξ,ζ1,ζ2(φ(ξ,ζ1,P1,...,Pn)∧φ(ξ,ζ2,P1,...,Pn) → ζ1 = ζ2) → ∀a∃b∀ζ(ζ ∈ b ↔ ∃ξ ∈ aφ(ξ,ζ,P1,...,Pn)));
10. Powerset axiom (POW):
∀a∃b(∀z(∃α(α ∈ z) ∧ ∀α(α ∈ z → α ∈ a) → ∃ξ∀β(β ∈ z ↔ g(β, ξ) ∈ b))).
In a model of ZFC the class of sets of ordinals together with the standard
relations <, =, and ∈, and the Go¨del pairing function G constitutes a model of SO. Note that the powerset axiom of SO requires the axiom of choice since it stipulates the existence of well-ordered powersets. Thus:
Theorem 5.2. The theory SO can be interpreted in the theory ZFC.
For the converse direction, which will be proved in the two subsequent sections, we first indicate that all basic mathematical notions can be reasonably formalized within the system SO. Beyond the specific requirements of the present paper, this also shows that the theory SO might have some wider interest as a foundational theory.
For the formalization of mathematics within SO we make use of the familiar class term notation A = {α|φ(α)} to denote classes of ordinals. If A = {α|φ(α)} is a non-empty class of ordinals let min(A) denote the minimal element of A. The existence of a unique minimum follows from the axioms (INI), (SEP) and (WO). (BOU) ensures the existence of an upper bound for each set a, the least of which will be noted lub(a). By (INI) the classes ια := {β|β < α} are sets. Using (SEP) and (INI), one sees that the union and intersection of two sets are again sets. Finite sets are denoted by {α0,α1,...,αn−1}. Their existence is implied by (INI) and (SEP). We write POW(b,a) for b being a set satisfying (POW) for a; note that in SO the set b is not uniquely determined by a. ω denotes the least element of the class of limit numbers which by (INF) is not empty. Finally let 0 := min({α| On(α)}), 1 := lub({0}), etc.
The inverse functions G1, G2 of G are defined via the properties α = G1(β) ↔ ∃γ(β = G(α,γ)) resp. α = G2(β) ↔ ∃γ(β = G(γ,α)). The axioms (GPF) and (SUR) imply the well-known properties of the Go¨del pair- ing function and its projections, such as bijectivity and monotonicity properties. To simplify notation, write (α, β) := G(α, β). Every set can be regarded as a set of pairs a = {(α,β)|(α,β) ∈ a} or more generally as a set of n-tuples. In this way n-ary relations and functions on ordinals can be represented by sets. We define further notions connected with relations and functions.