This chapter introduces the basic notions of effective computability from the set- theoretic perspective. While somewhat abstract at first sight, they are natural when viewed from the standpoint of definability.
An admissible structure is essentially an inner model of computation. The constructible universe L is defined via a transfinite iteration of the Gödel operators. By considering an appropriate initial segment of L which forms an admissible structure, we will see how a -set assumes the role of an r.e. set in higher recursion theory.
The Kripke–Platek (KP) theory of sets was developed by Kripke [75] and Platek [113]. KP is a weak version of the ZF axiom system and captures the basic features of effective computation in the setting of set theory. It offers a natural platform for the study in domains beyond ω.
Definition 3.1.1. Let denote the language of ZF. The collection of Δ0-formulas in is the smallest collection X consisting of the atomic formulas of and closed under the following operations:
(i)If φ ∈ X then ¬φ ∈ X.
(ii)If {φ, ψ}⊆ X, then {φ ∧ ψ, φ ∨ ψ} ⊆ X.
(iii)If φ ∈ X, then {(∀u ∈ v)φ, (∃u ∈ v)φ}⊆ X.
In (iii) above, both of the formulas (∀u ∈ v)φ, (∃u ∈ v)φ are called bounded formulas. A prefix of the form ∃u ∈ v or ∀u ∈ v is a bounded quantifier. Δ0-formulas are analogs of primitive recursive predicates in recursion theory.
Definition 3.1.2. A Δ0-formula is also known as a Σ0-formula as well as a Π0-formula. In general, a formula φ(u) is Σn+1 if it is of the form (∃v)ψ(u, v) where ψ is a Πn-formula. A formula φ(u) is Πn+1 if it is of the form (∀v)ψ(u, v) where ψ is a Σn-formula.
Definition 3.1.3. The class of Σ-formulas is the smallest class X consisting of the Δ0-formulas and closed under conjunction, disjunction, bounded quantification, and if φ ∈ X then (∃u)φ ∈ X.
The class of Π-formulas is the smallest class Xʹ consisting of the Δ0-formulas, closed under conjunction, disjunction, bounded quantification, and if φ ∈ Xʹ then (∀u)φ ∈ Xʹ.
Σ-formulas are analogs of recursively enumerable predicates in classical recursion theory. Note that there is a difference between a Σ1-formula and a Σ-formula. A Σ1-formula is a Σ-formula but not necessarily conversely.
Definition 3.1.4. The theory KP consists of the universal closure of the following formulas:
–Extensionality: (∀x)(∀y)((∀u)(u ∈ x ↔ u ∈ y) → x = y).
–Foundation: (∃x)φ(x) → (∃x)(φ(x) ∧ (∀y ∈ x)¬φ(y)), for all formulas φ in which y does not occur free.
–Pair: (∀x)(∀y)(∃z)(x ∈ z ∧ y ∈ z).
–Union: (∀x)(∃y)(∀u ∈ x)(∀v)(v ∈ u → v ∈ y).
–Δ0-separation: (∀x)(∃y)(∀u)(u ∈ y ↔ u ∈ x ∧ φ(u)), for all Δ0-formulas φ in which u does not occur free.
–Δ0-collection: (∀x)((∀u ∈ x)(∃v)φ(u, v) → (∃y)(∀u ∈ x)(∃v ∈ y)φ(u, v)),for all
Δ0-formulas φ in which y does not occur free.
Given a formula φ, we write φ(w) for the formula obtained upon replacing each unbounded quantifier in φ with a bounded quantifier restricted to w. Specifically, replace ∃u with ∃u ∈ w and ∀u with ∀u ∈ w. Clearly if φ is Σ, then ∃wφ(w) is Σ. Under KP, each Σ-formula is equivalent to a Σ1-formula, as given by the following theorem which is proved by induction on the complexity of formulas. We leave it as an exercise.
Theorem 3.1.5 (The Σ-reflection principle). Let φ be a Σ-formula. Then
KP ⊢ φ ↔(∃w)φ(w).
Hence the theorem asserts under KP the existence of a Δ0-definable set for a given Σ-formula. In fact, it says more:
Theorem 3.1.6 (The Σ-collection principle). Let φ be a Σ-formula and let a be a set, Then
KP ⊢(∀x ∈ a)(∃y)φ(x, y) → (∃w)((∀x ∈ a)(∃y ∈ w)φ(x, y)∧
(∀y ∈ w)(∃x ∈ a)φ(x, y)).
Proof. Assume that (∀x ∈ a)(∃y)φ(x, y). Then the formula (∀x ∈ a)(∃y)φ(x, y) is Σ. By Theorem 3.1.5, there is a set c such that (∀x ∈ a)(∃y ∈ c)φ(c)(x, y). Define b = {y | (∃x ∈ a)φ(c)(x, y)}. By Δ0-separation, such a b exists. It is straightforward to verify that φ(c)(x, y) implies φ(x, y) since φ(x, y) is Σ. Hence (∀y ∈ b)(∃x ∈ a)φ(x, y). Since (∀x ∈ a)(∃y ∈ c)φ(c)(x, y), we haveinfact (∀x ∈ a)(∃y)φ(c)(x, y). It follows that (∀x ∈ a)(∃y ∈ b)φ(c)(x, y).
Theorem 3.1.7 (The Δ-separation principle). Let a be a set. For any Σ-formula φ(x) and Π-formula ψ(x),
KP ⊢(∀x ∈ a)(φ(x)↔ ψ(x)) → (∃w)(∀x)(x ∈ w ↔ x ∈ a ∧ φ(x)).
Proof. Assume (∀x ∈ a)(φ(x) ↔ ψ(x)). Then (∀x ∈ a)(φ(x)∨¬ψ(x)). Note that the formula φ(x)∨¬ψ(x) is Σ. By Theorem 3.1.5, there is a set c such that (∀x ∈ a)φ(x)∨ ¬ψ(x) if and only if (∀x ∈ a)φ(c)(x)∨¬ψ(c)(x). Define b ={y | y ∈ a ∧ φ(c)(y)}. By Δ0-separation, such a b exists.
If y ∈ b, then y ∈ a ∧ φ(c)(y) and so y ∈ a ∧ φ(y) since φ(y) is Σ. If y ∈ a ∧ φ(y), then y ∈ a ∧ ψ(y) and so y ∈ a ∧ ψ(c)(y) since ψ is Π.
As seen in Chapters 1 and 2, definition by recursion using effective transfinite induction is a powerful tool in second order arithmetic. We now study definition by recursion in the setting of admissible set theory. This may be viewed as a generalization of recursion over .
Recall that a set x is transitive if (∀y)(∀z)(y ∈ x ∧ z ∈ y → z ∈ x). Note that the formula “x is transitive” is Δ0.
A function f is Σ if there is a Σ-formula φ such that f(x)= y ⇔ KP ⊢ φ(x, y). By Theorem 3.1.5, f is defined by a Σ1-formula. It is not difficult to see that if f is Σ, then for any set u,KP ⊢(∃v)(v = f ↾ u), where f ↾ u ={(x, y)| f(x)= y ∧ x ∈ u}).
Theorem 3.1.8. Let G be an n +2-ary Σ-function. There is an n +1-ary Σ-function F such that
KP ⊢ F(y, x1,…, xn)= G(y, x1,…, xn, {(z, F(z, x1,…, xn)) | z ∈ y}).]
Proof. Assume n = 0 for simplicity. Let P(f) be the sentence:
f is a function ∧ Dom(f) is transitive ∧
(∀y ∈ Dom(f)(f(y)= G(y, {(z, f(z)) | z ∈ y})).
Note that P(f) is a Σ-formula. Define
Q(y, z)=(∃f)(P(f)∧ f(y)= z),
and
F(y)= z ⇔ Q(y, z).
It suffices to show that
KP ⊢ F is a function ∧(∀y)(∃z)Q(y, z).
We show that KP ⊢(∀y)(∃z)Q(y, z). The other conjunct may be proved using a similar argument. Suppose KP does not prove (∀y)(∃z)Q(x, y, z). Then there is a model = 〈M, ∈〉 of KP such that ⊨ (∃y)(∀z)¬Q(x, y, z). By the Axiom of Foundation, choose y such that
Since Q(y, z) is Σ1, by Theorem 3.1.6, there is a v ∈ M such that
Hence there is a w ∈ M such that w ={f | f ∈ v ∧ P(f)}.
For any f1, f2 ∈ w and yʹ ∈ Dom(f1) ∩ Dom(f2), we claim that f1(yʹ) = f2(yʹ). Suppose not. Then by the Axiom of Foundation again, there is a yʹ such that f1(yʹ) ≠ f2(yʹ) but f1(yʺ)= f2(yʺ) for all yʺ ∈ yʹ. However,
f1(yʹ)= G(yʹ, {(yʺ, f1(yʺ)) | yʺ ∈ yʹ}) = G(yʹ, {(yʺ, f2(yʺ)) | yʺ ∈ yʹ}) = f2(yʹ),
a contradiction.
Now take . By Theorem 3.1.7, f ∈ M. Obviously, Dom(f) is transitive and so P(f). Define fʹ = f ∪{(y, G(y, f ↾ y))}. Then ⊨ fʹ(y)= G(y, f ↾ y)∧ P(fʹ) and so ⊨ (∃z)Q(y, z), a contradiction.
Thus KP ⊢(∀y)(∃z)Q(y, z).
Remark 3.1.9. Defining a function such as G in Theorem 3.1.8 quite often requires one to go through a series of straightforward, though tedious, steps of Σ1-induction. Henceforth we will leave the details of these steps to the reader and refer to them simply as “applying Theorem 3.1.8 by Σ1-induction”.
Theorem 3.1.8 is a central result in the theory of admissible sets. It plays the same role as that of effective transfinite induction in descriptive set theory. We illustrate this point with an application of the theorem. Define the transitive closure operator TC to be:
By induction on the relation ∈, one shows that for any set x, TC(x) is the smallest transitive set containing x. The question is whether this operator is well defined in KP.
Let G be a Σ-function such that G(, y) = and . Then by Theorem 3.1.8 there is a Σ-function F such that F(x)= G(x, {(y, F(y)) | y ∈ x}). It is not difficult to verify that for each x, F(x)= TC(x). We have the following corollary.
Corollary 3.1.10. KP ⊢ TC(x) is a Σ-function.
By Corollary 3.1.10, together with the proof of Theorem 3.1.8, we have the following theorem.
Theorem 3.1.11. Let G be an n + 2-ary Σ-function. There is an n + 1-ary Σ-function F such that
KP ⊢ F(y, x1,…, xn)= G(y, x1,…, xn, {(z, F(z, x1,…, xn)) | z ∈ TC(y)}).
Let rk be a function such that
By Theorem 3.1.8, rk is a Σ-function from sets to ordinals. For any set x, rk(x) is called the rank of x. The rank function is a convenient tool to use when performing transfinite induction.
A set x is transitive in z if y ∩ z ⊆ x for all y ∈ x. A set x is transitive if z = x, i.e. y ⊆ x for all y ∈ x. Using Theorem 3.1.8, we define a Σ-operation Cx(y) as follows:
It is easy to verify that Cb(b) is transitive for all b. Moreoverif a ⊆ b and a is transitive, then Cb(x)= x for all x ∈ a. Define cb ={(x, Cb(x)|x ∈ b}. One may view cb as a map from b onto the transitive set Cb(b). In general, cb is not injective.
A set a is extensional if for all b1, b2 ∈ a, (∀x ∈ a)(x ∈ b1 ↔ x ∈ b2)→ b1 = b2). In other words, a is extensional if each set in a is determined by its membership in a. Obviously, any transitive set is extensional. The following theorem says that any extensional set is isomorphic to a transitive set.
Theorem 3.1.12 (Mostowski [108]). If a is extensional then ca is a bijection between a and Ca(a). Furthermore, for all x, y ∈ a, x ∈ y ↔ ca(x)∈ ca(y).
Proof. Obviously ca is a surjective map from a to Ca(a) and x ∈ y implies ca(x)∈ ca(y). We show that for all x, y ∈ a, ca(x) ∈ ca(y) implies x ∈ y. Then by the extensionality of a, ca is injective.
Suppose there is a y0 ∈ a such that for all y ∈ a with rk(y) < rk(y0) and x ∈ a, x ∈ y ⇔ ca(x) ∈ ca(y) but there is an x0 ∈ a such that x0 ∉ y0 and ca(x0) ∈ ca(y0). Since ca(x0) ∈ ca(y0), there is a z ∈ a∩y0 such that ca(x0)= ca(z). Then rk(z) < rk(y0). However, this implies x0 = z ∈ y0, a contradiction.
Denote by M the domain of a structure .
Definition 3.1.13. Let be a set of formulas in .
(i)Given a structure and A ⊆ M, we say that A is -definable in if there is a formula φ(u, v0,…, vn) ∈ and a finite sequence a0,…, an in M such that x ∈ A if and only if ⊨ φ(x, a0,…, an);
(ii)if is a collection of structures and AM ⊆ M for , then is -uniformly definable in if there is a formula φ(u) in without parameters such that for any if and only if ⊨ φ(x).
Note that for a collection of structures to be uniformly definable, there should be no parameters in the formula defining it.
Definition 3.1.14. Given a set of sentences in , we say that two -structures and are -elementarily equivalent, written , if for every φ ∈ ,
If is the set of all sentences, then we say that and are elementarily equivalent and write ≡ .
Definition 3.1.15. Given a set of sentences , we say that an embedding j from into is -elementary and write if for every and finite sequence ,
If is the set of all formulas, then we write . If j is the inclusion map, then we write ≺ and say that is an elementary substructure of , and is an elementary extension of .
Definition 3.1.16. Given a class of structures and a formula ,
(i)φ is -upward absolute if for every pair ⊆ in and any finite sequence implies ;
(ii)φ() is -downward absolute if for every pair ⊆ in and any finite sequence implies ;
(iii)φ() is -absolute if it is both -upward and downward absolute.
Proposition 3.1.17. Let be a class of transitive structures.
(i)Every Σ0-formula is -absolute;
(ii)every Σ1-formula is -upward absolute;
(iii)every Π1-formula is -downward absolute.
Hence every Δ1-formula is -absolute.
Proof. We prove (i) by induction on the complexity of Σ0-formulas and leave (ii) and (iii) to the reader. Suppose ⊆ and φ(a) has the form (∃u ∈ a)ψ(u, a) for some Σ0-formula ψ(u, a) with a ∈ M. If ⊨ φ(a), then there exists an aʹ ∈ M such that ⊨ ψ(aʹ, a). Since ⊆ , by induction ⊨ ψ(aʹ, a). If ⊨ φ(a), then there exists an aʹ ∈ N such that ⊨ ψ(aʹ, a). Since aʹ ∈ a and a ∈ M, by transitivity we have aʹ ∈ M. Then by induction, ⊨ ψ(aʹ, a).
Further facts concerning KP may be found in [3].
Exercise 3.1.1. Prove Theorem 3.1.5.
Exercise 3.1.2. Complete the proof of Proposition 3.1.17.
The universe of sets V is defined inductively on ordinals:
Definition 3.2.1. An admissible structure (or an admissible set) is a model of KP of the form = 〈, ∈M〉 where M is a transitive set in V and ∈M is the restriction of ∈ to M. We will often write ∈M simply as ∈ if the context is clear.
Definition 3.2.2. The ordinal of a transitive structure , denoted o(), is the least ordinal not in M. An ordinal α is admissible if α = o() for some admissible structure .
A relation S ⊆ Mn on is Σn if there is a Σn-formula φ such that
We allow parameters in the above definition. Clearly both a and {a} are Σ1 for any a ∈ M. Moreover, it follows from Theorem 3.1.5 that for admissible, Σ1-relations are closed under ∨, ∧, ∃x ∈ a, ∀x ∈ a and ∃x.
Definition 3.2.3. A set a ∈ V is hereditarily finite, written a ∈ HF, if TC(a) is finite.
HF can be redefined by induction as follows:
Thus HF = Vω. We leave the following theorem as an exercise.
Theorem 3.2.4. HF is the smallest admissible set.
〈HF, ∈〉 is the first natural example of an admissible set we encounter. There is a natural and standard way of identifying n as a natural number (in arithmetic) and n as a finite ordinal (in set theory). We will follow the convention of identifying these two objects. The following theorem highlights an important connection between recursion theory and admissibility theory, and explains the reason for introducing admissible sets in the study of generalized recursion theory.
Theorem 3.2.5. Let S be a relation on the natural numbers. Then S is r.e. if and only if S is Σ1 over 〈HF, ∈〉.
Proof. It is sufficient to assume that S is infinite. The class of r.e. relations is the class of relations which are Σ1-definable over 〈ω, +, ⋅,0,1, <〉 in the language of first order arithmetic. Thus for the “only if” part, it is sufficient to show that if S ⊆ ω is Σ1 over (ω, +, ⋅,0,1, <), then it is Σ1 over 〈HF, ∈〉 in the language of set theory. It is obvious that the set of ordinals in HF, i.e. ω, is Δ1-definable over 〈HF, ∈〉. Now it is routine to show that if S is defined by an open formula φ involving +, ⋅, then it is defined over 〈HF, ∈〉 by a Δ1-formula φ∗ in the language of set theory. Also “u < v” is definable over 〈HF, ∈〉 by “u ∈ v”. Hence any open formula defining S involving +, ⋅, < is definable by a corresponding Δ1-formula over 〈HF, ∈〉 in the language of set theory.
For S defined by a bounded formula φ of the form (∃i < n)ψ where ψ is open, let φ∗ be (∃u ∈ n)ψ∗(u), where ψ∗ is the Δ1-formula corresponding to ψ (note that the “n” in φ∗ denotes the finite ordinal n). Define φ∗ for φ of the form (∀i < n)ψ and ψ open, in the obvious way. By induction on the complexity of formulas, any S ⊆ ω defined by a bounded formula in the language of first order arithmetic has a corresponding definition via a Δ1-formula in the language of set theory over 〈HF, ∈〉.
Now assume that S = {m|(∃i)ψ(i, m)} where ψ is a bounded formula in arithmetic. By induction, let ψ∗ be a Δ1 such that 〈ω, +, ⋅,0,1, <〉 ⊨ ψ(n, m) if and only if 〈HF, ∈〉 ⊨ ψ∗(n, m). Then m ∈ S if and only if
Hence S is Σ1 over 〈HF, ∈〉.
For the other direction, we first define a function f : ω → HF as follows:
It is straightforward to verify that f is a bijection. Furthermore,
–f is Δ1 over 〈HF, ∈〉.
–Define f ∗(n)= m if and only if m as an ordinal is the set f(n). Then the relation “f ∗(n)= m” is recursive.
–The set Tφ ={(n1, n2,…, nk)|〈HF, ∈〉 ⊨ φ(f(n1), f(n2),…, f(nk))} is recursive for each Δ0-formula φ.
Now if S is Σ1 over 〈HF, ∈〉, then there is a Δ0-formula φ such that S(m) if and only if there is a u ∈ HF with 〈HF, ∈〉 ⊨ φ(u, m). Thus S(m) if and only if (∃i)(∃j)(f ∗(i)= m ∧(i, j)∈ Tφ). We conclude that S is an r.e. relation.
By the proof of Theorem 3.2.5, we have the following result.
Proposition 3.2.6. For any S ⊆ HF, there is an xS ⊆ ω such that S is Δ1-definable in 〈HF, ∈, xS〉 and xS is Δ1-definable in 〈HF, ∈, S〉.
Proof. By the proof of Theorem 3.2.5, there is a bijection f : ω ↦ HF which is Δ1-definable in 〈HF, ∈〉. Define n ∈ xS if and only if f(n)∈ S.
Model-theoretically, Theorem 3.2.5 may be viewed as a biinterpretation of Σ1-formulas between 〈HF, ∈〉 and 〈ω, ∈〉 (see [52]).
Exercise 3.2.1. Prove Theorem 3.2.4.
The constructible universe L was introduced by Gödel [37] to prove the consistency of the Generalized Continuum Hypothesis and the Axiom of Choice. Jensen [55] developed the fine structure theory of L and the theory has had a deep impact on higher recursion theory.
Expand the language of set theory with a unary relation symbol and denote it as .
Definition 3.3.1. Let A bea set. Given A set X, we say that Y is definable relative to A over the structure (X, ∈, A ∩ X), written Y ∈ Def A(X), if there is a formula φ(v) in such that upon interpreting to be A ∩ X, we have Y = {y |〈X, ∈, A ∩ X〉 ⊨ φ(y)}.
By recursion on ordinals, define
Define L[A]= ⋃β Lβ[A], and L = L[]. Obviously L[A] is a proper class.
If x ∈ L[A], then x is said to be A-constructible. In particular, x is constructible if A = . The construction of L is uniformly Σ1-definable over any admissible structure , in the sense of the following theorem whose proof we omit. It involves a tedious coding device that is Σ1-definable by appealing to Theorem 3.1.8. For details, see [22].
Theorem 3.3.2. There exists a Σ1-formula φ(u, v) such that for any admissible structure and ordinal β ∈ M, ⊨ φ(β, x) if and only if x = Lβ. Moreover, Lβ is the unique set such that ⊨ φ(β, x). Hence Lβ is uniformly Δ1-definable over .
There is a recursion-theoretic way of generating L via the following set of primitive recursive operators introduced by Gödel:
(i)F0(x, y)={x, y}.
(ii)F1(x, y)= x y.
(iii)F2(x, y)= x × y ={x, {x, y}}.
(iv)F3(x, y)={(u, z, v)| z ∈ x ∧(u, v)∈ y}.
(v)F4(x, y)={(u, v, z)| z ∈ x ∧(u, v)∈ y}.
(vi)F5(x, y)= ⋃ x.
(vii)F6(x, y)={y |∃z(y, z)∈ x}.
(viii)F7(x, y)=∈∩ x × x.
(ix) F8(x, y)={z1 |∃z0((z0, z1)∈ x ∧ z0 ∈ y)}.
(x)F9(x) = A ∩ x.
Let
and
If A = , then we write J for J[A]. Intuitively and according to Jensen [55], Jβ+1 is the result of “stretching” the collection of the definable subsets of Jβ upwards by ω-levels in rank without adding new sets. The proof of the following proposition may be found in [22].
Proposition 3.3.3. For all β,
–Jβ[A] is transitive.
–There is a Σ1-formula φ(u, w) such that for any two ordinals ν < β, 〈Jβ, ∈〉 ⊨ φ(ν, x) if and only if x = Jν;
–There is a Σ1-formula φ<(u, v) such that
(i) for any β, φ<(u, v) defines a well-ordering <Jβ on Jβ;
(ii) for any ν > β, if y ∈ Jβ and 〈Jν, ∈〉 ⊨ φ<(x, y), then x ∈ Jβ and 〈Jβ, ∈〉 ⊨ φ<(x, y).
–Theorem 3.3.2 remains true for Jβ;
–Jβ+1[A]∩ P(Jβ[A]) = DefA(Jβ[A]).
–Lβ[A]⊆ Jβ[A]⊆ Lωβ.
–Jβ[A]= Lβ[A] if and only if ωβ = β.
–L[A]= ⋃β Jβ[A];
–Theorem 3.3.2 remains valid for J.
The Gödel operators provide an algorithmic approach to the construction of L. It reveals the “black box” hidden within the reference to definability. Based on Proposition 3.3.3, we may think of L as being obtained by an effective transfinite induction over the class of ordinals, analogous to the way hyperarithmetic sets are defined over . This connection is useful as it suggests initial segments of L as models of computation in the general setting.
If one works within a structure and performs the stage-by-stage construction of L, then one arrives at the same Lβ for each β ∈ M if satisfies a sufficiently strong condition such as admissibility. The following theorem formalizes this idea. Let (Lβ)M denote the Lβ constructed in .
Theorem 3.3.4. Let be a transitive model of KP. Then for each β < o(M), Lβ ∈ M and (Lβ)M = Lβ.
Proof. By Theorem 3.3.2, the formula “x = Lβ” is Δ1-definable over . By the absoluteness of Δ1-formulas, Lβ ∈ M and (Lβ)M = Lβ.
Corollary 3.3.5. Suppose is transitive, admissible and ⊨ “V = L”. Then M = Lα where α = o(M).
Theorem 3.3.6. α is admissible if and only if 〈Lα, ∈〉 is admissible.
Proof. If 〈Lα, ∈〉 is admissible, then α is admissible.
If α = o() for some admissible , then (Lβ)M = Lβ for each β < α by Theorem 3.3.4. Hence it suffices to show that Lα = ⋃β<α(Lβ)M is admissible. We verify that Δ0-collection holds in Lα and leave the verification of other properties to the reader.
Suppose that 〈Lα, ∈〉 ⊨ (∀x ∈ a)(∃y)φ(x, y). By the absoluteness of Δ0-formulas, for each x ∈ a, there is a (least) β < α such that
⊨ (∃y ∈ Lβ)φ(x, y).
Then Theorem 3.3.2 and Theorem 3.1.6 on Σ-collection imply that there is an α0 < α such that a ∈ Lα0 and
⊨ (∀x ∈ a)(∃β < α0)(∃y ∈ Lβ)φ(x, y).
The absoluteness of Δ1-formulas now gives
〈Lα0, ∈〉 ⊨ (∀x ∈ a)(∃y)φ(x, y).
Then {y |〈Lα0, ∈〉 ⊨ (∃x ∈ a)φ(x, y)} ∈ Lα0+1 and is contained in Lα.
Obviously if α = ω, then Lα = HF. Hence Lω is the smallest admissible set (cf. Theorem 3.2.4). Note that if α > ω is admissible, then ωα = α.
A fundamental property of L is the following known as condensation:
Theorem 3.3.7. Suppose that β > 0 and 〈X, ∈〉 ≺Σ1 〈Jβ, ∈〉. Then 〈X, ∈〉 ≅ 〈Jγ, ∈〉 for some γ ≤ β. Moreover π(x) ≤ Jβ x for every x ∈ X.
Proof. Suppose 〈X, ∈〉 ≺Σ1 〈Jβ, ∈〉. Then 〈X, ∈〉 is wellfounded and satisfies the extensionality axiom. By Theorem 3.1.12, there is a transitive set M such that
π : 〈X, ∈〉 ≅ 〈M, ∈〉.
We claim that M = Jγ where γ = sup{π(δ)| δ ∈ β ∩ X}.
Clearly and M is transitive. By Proposition 3.3.3, there is a Σ0-formula φ(x, δ, s) such that for any x ∈ Jβ and δ < β, 〈Jβ, ∈〉 ⊨ ∃sφ(x, δ, s) if and only if x = Jδ. Since M is transitive, by an induction on δ < γ, we prove that Jδ ∈ M for any δ < γ. Hence Jγ ⊆ M.