Page 66 - Textos de Matemática Vol. 38

58 PETER KOEPKE
Theorem 4.5. Let the function f : Ordn → Ord be ordinal register computable and surjective. Then there are ordinal register computable functions g0,...,gn−1 : Ord → Ord such that
∀αf(g0(α),...,gn−1(α)) = α. 5 The theory SO of sets of ordinals
Ordinal Turing computations do not directly produce highly hierarchical sets but ordinals and sets of ordinals. It is well-known that a model of Zermelo- Fraenkel set theory with the axiom of choice (ZFC) is determined by its sets of ordinals [6], Theorem 13.28. This motivates the formulation of a theory SO which axiomatizes the sets of ordinals in a model of ZFC. The theory SO is two-sorted where the intended interpretations are ordinals and sets of ordinals. Let LSO be the language
LSO :={On,SOn,<,=,∈,g}
where On and SOn are unary predicate symbols, <, =, and ∈ are binary predi- cate symbols and g is a two-place function. The intended standard interpretation of g is given by the Go¨del pairing function G. To simplify notation, we use lower case greek letters to range over elements of On and lower case roman letters to range over elements of SOn.
Definition 5.1. The Theory SO is formulated in the first-order language LSO and consists of the following list of axioms:
1. Well-ordering axiom (WO):
∀α, β, γ(¬α < α ∧ (α < β ∧ β < γ → α < γ) ∧
(α < β ∨ α = β ∨ β < α)) ∧
∀a(∃α(α ∈ a) → ∃α(α ∈ a ∧ ∀β(β < α → ¬β ∈ a)));
2. Axiom of infinity (INF) (existence of a limit ordinal): ∃α(∃β(β < α) ∧ ∀β(β < α → ∃γ(β < γ ∧ γ < α)));
3. Axiom of extensionality (EXT): ∀a, b(∀α(α ∈ a ↔ α ∈ b) → a = b);
4. Initial segment axiom (INI): ∀α∃a∀β(β < α ↔ β ∈ a);
5. Boundedness axiom (BOU): ∀a∃α∀β(β ∈ a → β < α);
6. Pairing axiom (GPF) (G¨odel Pairing Function):
∀α,β,γ(g(β,γ) ≤ α ↔ ∀δ,ǫ((δ,ǫ) <∗ (β,γ) → g(δ,ǫ) < α)).
Here (α, β) <∗ (γ, δ) stands for
∃η, θ(η = max(α, β) ∧ θ = max(γ, δ) ∧ (η < θ ∨
(η = θ ∧ α < γ) ∨ (η = θ ∧ α = γ ∧ β < δ))),
where γ = max(α, β) abbreviates (α > β ∧ γ = α) ∨ (α ≤ β ∧ γ = β);