Corrections to my article “Ordinal Systems”

Anton Setzer^{∗}

January 25, 2001

Unfortunately Markus Michelbrink, Hannover, Prof. H. Schwichtenberg, Munich, and myself have detected some mistakes in the article Anton Setzer, Ordinal systems, in Cooper, B. and Truss, J. (Eds.): Sets and proofs, Cambridge University Press, Cambridge, pp. 301 – 331, 1999 of which one is a crucial cut-and-paste error in the definition of ordinal systems.

A corrected version is available via my home page (see below). The list of corrections follows.

Abstract, line 6 – 7 Replace “transfinitely iterated fixed point theories |ID_{σ}|” by “theories of transfinitely iterated inductive definitions |ID_{σ}|”.

Def. 1.1 (a) For clarification insert the following text after the paragraph defining what a class is: “A binary relation ≺ is a class. For binary relations ≺ we define r ≺ s := π(r, s) ∈≺, where π is a standard primitive recursive pairing function on the natural numbers having the usual properties.” Add further before “Transfinite induction over (A, ≺) is in PRA reducible to transfinite induction over (A_{i}, ≺_{i}) (i = 1, …, n), …” the following sentence: “Let A be a class, ≺ be a binary relation, both depending on unary free predicates A_{i} and binary free predicates ≺_{i} (i = 1, …, n).”

Def. 1.1 (b) This part has to be rewritten as follows:

“Assume B is a class and ≺ is a binary relation, both depending on unary free predicates A_{i} and binary free predicates ≺_{i} (i = 1, …, m). (B, ≺) is an elementary construction from (A_{1}, ≺_{1}), …, (A_{m}, ≺_{m}), if the following holds: the formulas defining B, ≺ are formulas of the language of PRA with bounded quantifiers only (ie. quantifiers of the form ∀x < t, ∃x < t); PRA^{+} proves that, if (A_{i}, ≺_{i}) are linear orderings (i = 1, …, m), so is (B, ≺); transfinite induction over (B, ≺) is PRA-reducible to transfinite induction over (A_{i}, ≺_{i}).”

Def. 1.1 (j) “⋃{X ⊆ |A| | (X, ≺) well-ordered }” instead of “⋂{X ⊆ |A| | (X, ≺) well-ordered }”.

Def. 2.1 (d) Replace in (OS 1) and (OS 3) “Arg” by “T”.

Sect. 2.2, line 9/10 Replace “(more precisely the formula ∀n ∈ ℕ(n ≤ \underline{n} ∧ ∀x ∈ T(x < \underline{n} ↔ ∃l < n.x = \underline{l})) is provable in PRA).” by “(more precisely the formula ∀n ∈ ℕ(n ≤ \underline{n} ∧ ∀x ∈ T(x ≺ \underline{n} ↔ ∃l < n.x = \underline{l})) is provable in PRA).”

∗Department of Mathematics, Uppsala University email: setzer@math.uu.se, home page:

http://www.math.uu.se/∼setzer

Lem. 2.2 (a), line 1/2 Omit “Let b ∈ T”. Lem. 2.2 (a), line 4 Replace

“∀α, β < γ(α < β → a_{α} ≺′ a_{β})” by “∀α, β < γ(α < β → a_{α} ≺ a_{β})”.

Proof of Lem 2.2, (a), line 10 Replace “k(b) ≺ b ≺ a” by “k(b) ≺ b ≺ a_{δ}”.

Lem. 2.8 (a) Replace “∀a ∈ T′.k̂(a) ⊆ T” by “∀a ∈ T′.l̂(a) ⊆ k̂(a) ⊆ T”.

Lem 2.8 (b) line 1 Replace “∀a ∈ T′(f[k̂(a)] = k^{0}(f(a)) ∧ f[l̂(a)] = l′(f(a)))” by “∀a ∈ T′(f[k̂(a)] = k^{0}(f(a)) ∧ f[l̂(a)] = l(f(a)))”.