{'fraction_non_alphanumeric': 0.046688295482904915, 'fraction_numerical': 0.003923134514599451, 'mean_word_length': 4.590178571428571, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle/ZF

The proof of the relative consistency of the axiom of choice has been mechanized using Isabelle/ZF. The proof builds upon a previous mechanization of the reflection theorem. The heavy reliance on metatheory in the original proof makes the formalization unusually long, and not entirely satisfactory: two parts of the proof do not fit together. It seems impossible to solve these problems without formalizing the metatheory. However, the present development follows a standard textbook, Kunen's Set Theory, and could support the formalization of further material from that book. It also serves as an example of what to expect when deep mathematics is formalized.


Introduction
In 1940, Gödel [5] published his famous monograph proving that the axiom of choice (AC) and the generalized continuum hypothesis (GCH) are consistent with respect to the other axioms of set theory. This theorem addresses the first of Hilbert's celebrated list of mathematical problems. I have attempted to reproduce this work in Isabelle/ZF.
When so much mathematics has already been checked mechanically, what is the point of checking any more? Obviously, the theorem's significance makes it a challenge, as does its size and complexity, but the real challenge comes from its reliance on metamathematics. As I have previously noted [18], some theorems seem difficult to formalize even in their statements, let alone in their proofs. Gödel's work is not a single formal theorem. It consists of several different theorems which, taken collectively, can be seen as expressing the relative consistency of the axiom of choice. At the end of Chapter VII, Gödel remarks that given a contradiction from the axioms of set theory augmented with AC, a contradiction in basic set theory "could actually be constructed" [5, p. 87]. This claim is crucial: logicians prefer consistency proofs to be constructive.
Gödel's idea [4,6] is to define a very lean model, called L, of set theory. L contains just the sets that must exist because they can be defined by formulae. Then, prove that L satisfies the ZF axioms and the additional axiom "every set belongs to L," which is abbreviated V = L. We now know that V = L is consistent with ZF, and can assume this axiom. (The conjunction of ZF and V = L is abbreviated ZFL.) We conclude by proving that AC and GCH are theorems of ZFL and therefore are also consistent with ZF.
A complication in Gödel's proof is its use of classes. Intuitively speaking, a class is a collection of sets that is defined by comprehension, { | ( )}. Every set is trivially a class, namely { | ∈ }, but a proper class is too big to be a set. Formal set theories restrict the use of classes in order to eliminate the danger of paradoxes. Modern set theorists use Zermelo-Fraenkel (ZF) set theory, where classes exist only in the metalanguage. That is, the class { | ( )} is just an alternative notation for the formula ( ), and ∈ { | ( )} is just an alternative notation for ( ). The universal class, V, corresponds to the formula True. An "equation" like V = ∈ON stands for ∀ . ∃ . ON( ) ∧ ∈ . (Here, ON denotes the class of ordinal numbers.) Gödel's monograph [5] uses von Neumann-Bernays-Gödel (NBG) set theory, which allows quantification over classes but restricts their use in other ways. With either axiom system, classes immensely complicate the reasoning, making it highly syntactic.
Why did Gödel use classes? Working entirely with sets, he could have used essentially the same techniques to prove that if is a model of ZF then there ex-ists a model ( ) of ZFC. (ZFC refers to the ZF axioms plus AC.) Therefore, if ZFC has no models, then neither does ZF. But with this approach, he can no longer claim that if he had a contradiction in ZFC then a contradiction in ZF "could actually be constructed." 1 For the sake of this remark, which is not part of any theorem statement, Gödel chose a more difficult route. Classes create more difficulties for formal proof checkers (which have to face foundational issues squarely) than they do for mathematicians writing in English. The proof uses metatheoretic reasoning extensively. Gödel writes [5, p. 34], However, the only purpose of these general metamathematical considerations is to show how the proofs for theorems of a certain kind can be accomplished by a general method. And, since applications to only a finite number of instances are necessary . . ., the general metamathematical considerations could be left out entirely, if one took the trouble to carry out the proofs separately for any instance.
I decided to take the trouble, not using metatheory but relying instead on a mechanical theorem prover. This paper describes the Isabelle/ZF proofs. It indicates the underlying mathematical ideas and sometimes discusses practical issues such as proof length or machine resources used. It necessarily omits much material that would be too long or too repetitious. The paper concerns how existing mathematics is formalized; it contains no original mathematics.
Overview. The paper begins by outlining Gödel's relative consistency proof ( §2). After a brief overview of Isabelle/ZF, the paper describes the strategy guiding the formalization ( §3) and presents some elementary absoluteness proofs ( §4). It then discusses relativization issues involving well-founded recursion ( §5). Turning away from absoluteness, the paper proceeds to describe the formalization of the constructible universe and the proof that L satisfies the ZF axioms ( §6); then, it describes how the reflection theorem is used to prove that L satisfies the separation axiom ( §7). Absoluteness again takes centre stage as the paper presents the relativization of two essential datatypes ( §8) and finally presents the absoluteness of L itself ( §9). Finally, the paper presents the Isabelle proof that AC holds in L ( §10), and offers some conclusions ( §11).

Proof Outline
Recall that Gödel's idea is to define a lean model of set theory, the class L of the constructible sets. Figure 1 shows L (shaded) as a subclass of the universe, V. The vertical line represents the class ON of the ordinals.
Gödel's proof involves four main tasks: 1. defining the class L within ZF 2. proving that L satisfies the ZF axioms 3. proving that L satisfies V = L 4. proving that V = L implies the axiom of choice As we shall see, Isabelle is well-suited for completing the first and last parts. Both the definition of L and the proof of the axiom of choice are straightforward exercises in mechanized set theory. The second task cannot quite be completed: all of the ZF axioms can be verified apart from separation, which is an axiom scheme, and each instance requires its own proof. As for the third task, the Isabelle proof that L satisfies V = L is much longer than I would like because the metamathematical techniques that abbreviate textbook proofs are not available. Once we have completed the first three tasks, we should be able to conclude that if ZF is consistent, then so is ZFL. (And from the fourth task, if ZF is consistent, then so is ZFC.) This inference requires reasoning in the metatheory, which is not possible using Isabelle/ZF, so the machine formalization omits it. Standard treatments also gloss over this step, regarding it as obvious. Section 2.4 below expands on this issue. 7

The Problem With Class Models
Because L is a proper class, we cannot adopt the usual notion of satisfaction. To formalize the standard Tarski definition of truth [10, p. 60] requires first defining, in set theory, a set to represent the syntax of first-order formulae.
is easily defined, either using Gödel-numbering or as a recursive data structure. If is a set, ∈ represents a formula with free variables, and 1 , . . . , ∈ then |= ( 1 , . . . , ) can be defined by recursion on the structure of . If M is a proper class, then the obvious definition of M |= ( ì ) cannot be formalized in set theory; the environments that hold the bindings of free variables would have to belong to a function space whose range was all of M. Tarski's theorem on nondefinability of truth [9, p. 41] asserts that no formula ( ) expresses V |= . If for each formula we write for the corresponding element of , then ↔ ¬ ( ) is a theorem for some sentence . Satisfaction cannot be defined, at least if M = V.

Relativization
Gödel instead expressed satisfaction for class models syntactically. This approach abandons the set of formula representatives in favour of real formulae. Set theory uses a first-order language with no constant symbols, no function symbols and no relation symbols other than ∈ and =. Variables are the only terms.
Gödel's key concept is relativization. 2 If M is a class and is a formula, define M recursively as follows:

The Formal Treatment of Terms
Despite the lack of terms in their formal language, set theorists use elaborate notational conventions. In other branches of mathematics, an expression like ( ) ( ) − ℎ( , ) means what it says: functions , and ℎ are applied and the results combined by multiplication and subtraction. But in set theory, each expression ( ) abbreviates a formula ( , ), which reduces the meaning of = ( ) to a combination of ∈ and =. For example, we can express the meaning of = ∪ by the predicate union( , , ), defined by ∀ . ∈ ↔ ∈ ∨ ∈ .
Variable binding notation, ubiquitous in set theory, causes complications. In ∈ ( ), what is ? Syntactically, ( ) is a term with parameter , so we can take it as an abbreviation for some formula ( , ). But then becomes an operation on formulae rather than one on sets. An equally legitimate alternative [7, p. 34] is to regard as a function in set theory -formally, the set of pairs { , ( ) | ∈ }.
Set theorists generally say little about these notational conventions and act as if terms were meaningful in themselves. But relativization forces us to make the translation from terms to formulae explicit. In the Isabelle formalization, I have defined relational equivalents of dozens of term formers. I have included a class argument in each one to perform relativization at the same time; we can express the relativized term (( ∪ ) ∩ ) M as ∃ ∈ M. union(M, , , ) ∧ inter(M, , , ) The hardest tasks were (1) to define relational equivalents of the complicated expressions generated by Isabelle/ZF for recursively defined sets and functions and (2) to cope with the sheer bulk of the definitions.

Gödel's Claim Viewed Proof-Theoretically
The purpose of relativization is to express claims of the form " is true in M." To prove that L satisfies the ZF axioms and V = L, we must prove L for each ZF axiom , and we must prove (V = L) L . Now we can consider Gödel's claim that from a contradiction in ZFL a contradiction in ZF "could actually be constructed." His claim is proof-theoretic. A contradiction in ZFL is a proof, Π, of ⊥ from finitely many ZF axioms and V = L: Once we have proved that L satisfies the axioms of ZFL, we have the + 1 proofs Verifying Gödel's claim reduces to showing that we can always construct a proof Π L of ⊥ L from the relativized premises: For then we get a proof of ZF ⊥ L , which is just ZF ⊥. So how we obtain Π L from Π? To be concrete, suppose we are working with a natural deduction formalization of first-order logic. By the normal form theorem [20], since the conclusion of the proof is atomic, we can assume that Π applies only elimination rules. We must modify Π so that it accepts relativized versions of its premises and delivers a relativized version of its conclusion. The only hard cases involve quantifiers. Where Π applies the existential elimination rule to ∃ . ( ), it delivers the formula ( ) to the rest of the proof. (Assume that has already been renamed, if necessary.) At the corresponding position, Π L should apply the existential and conjunction elimination rules to ∃ . ∈ L ∧ ( ), delivering the formulae ∈ L and ( ) to the rest of the proof.
Universal quantifiers require a bit more work. First, recall that the language of set theory has no terms other than variables. Where Π applies the universal elimination rule to ∀ . ( ), it delivers the formula ( ) to the rest of the proof, where is a variable. At the corresponding position, Π L should apply the existential and conjunction elimination rules to ∀ . ∈ L → ( ). But before it can deliver the formula ( ), it requires a proof of ∈ L. We will indeed have ∈ L if the variable is obtained by a previous existential elimination, but what if was chosen arbitrarily? We can handle such cases by inserting at this point an application of the empty set axiom, which will yield a new variable (say ) and the assumption ∈ L. Intuitively, we are replacing all free variables in Π by 0.
The sketchy argument above cannot be called a rigorous proof of Gödel's claim. But it is more detailed than standard expositions of Gödel's proof. Kunen relegates the relevant lemma to an appendix, and for the proof he merely remarks "Similar to the easy direction of the Gödel Completeness Theorem" [9, p. 141]. To Gödel, it was all presumably trivial. I have not formalized the argument in Isabelle/ZF because that would require formalizing the metatheory.

Defining the Class L
The equation V = ∈ON expresses the universe of sets as the union of the cumulative hierarchy { } ∈ON , which is recursively defined by 0 = 0, +1 = P ( ) and = < when is a limit ordinal. We obtain L by a similar construction, replacing the powerset operator P by the definable powerset operator, D. Essentially, D ( ) yields the set of all subsets of that can be defined by a formula taking parameters over . If we define the set of formulae and the satisfaction relation |= as outlined above, then we can make the definition (The ellipsis can be eliminated in favour of lists over .) Finally, we define the constructible universe: L = ∈ON , where 0 = 0, +1 = D ( ) and = < when is limit. Kunen proves that L satisfies the ZF axioms, remarking [9, p. 170] "only the Comprehension Axiom required any work." His remark applies to the Isabelle/ZF proofs. L inherits most of the necessary properties from V. Even the axiom scheme of replacement can be proved as the theorem replacement(L,P); the proof is independent of the formula P. However, the proof of comprehension for the formula requires an instance of the reflection theorem for , which requires recursion over the structure of . Each instance of comprehension therefore has a different proof from the ZF axioms. At the metalevel, of course, all these proofs are instances of a single algorithm. For Isabelle/ZF, this means that each instance of comprehension must be proved separately, although the proof scripts are nearly identical.

Absoluteness: Proving (V = L) L
Proving that L satisfies V = L is a key part of the proof, and despite first appearances, it is far from trivial. It amounts to saying that the construction of L is idempotent: L L = L. The underlying concept is called absoluteness, which expresses that a given operator or formula behaves the same in a class model M as it does in V, the universe. A class M is transitive if ∈ M implies ⊆ M, and we shall only be concerned with transitive models below.
Most constructions are absolute. The empty set can only be a set having no elements, and ⊆ can only mean that every element of belongs to . If and are sets then their union can only be the set containing precisely the elements of those sets. Many complicated notions are also absolute: domains and ranges of relations, bijections, well-orderings, order-isomorphisms, ordinals. With some effort, we can show the absoluteness of recursively defined data structures and functions.
Powersets, except in trivial cases, are not absolute. For example, P ( ) might contain subsets of the natural numbers that cannot be shown to exist. The function space → is not absolute because of the obvious connection between P ( ) and → {0, 1}. More subtly, cardinality is not absolute: if is a countable model of set theory, and is an uncountable cardinal according to , then obviously must be really be countable, with the bijections between and lying outside . This situation is called Skolem's paradox [9, p. 141].
Metamathematical arguments are an efficient means of proving absoluteness. For example, any concept that is provably equivalent (in ZF) to a formula involving only bounded quantifiers is absolute [9, p. 119]. This is the class of Δ ZF 0 formulae. The larger class of Δ ZF 1 formulae can also be shown to be absolute. Unfortunately, all such arguments are beyond our reach unless we formalize the metatheory.

The Consequences of V = L
Once we have proved that L is absolute, we obtain ZF (V = L) L . We can then investigate the consequences of assuming V = L. To prove the axiom of choice, it suffices to prove that every set can be well-ordered. The key step, given a well-ordering of , is to construct a well-ordering of D ( ). It comes from the lexicographic ordering on tuples , 1 , . . . , for ∈ and 1 , . . . , ∈ . So if is well-ordered, so is +1 . By transfinite induction, each level of the construction of L is well-ordered.
The axiom V = L is very strong. Gödel proved that it implies the generalized continuum hypothesis. Jensen later proved that it implies the combinatorial principle known as ♦, and it has many additional consequences. But it is important to note that such proofs are entirely separate from that of ZF (V = L) L . We prove ZFL AC, ZFL GCH and ZFL ♦, but we do not prove ZF AC L , ZF GCH L and ZF ♦ L . Those results, if we want them, are most easily obtained in the metatheory, using the general fact that if then L L .

Introduction to the Isabelle/ZF Formalization
Isabelle [11,14] is an interactive theorem prover that supports a variety of logics, including set theory and higher-order logic. Isabelle provides automatic tools for simplification and logical reasoning. They can be combined with single-step inferences using a traditional tactical style or as structured proof texts. The Proof General user interface provides an effective interactive environment. Isabelle has been applied to a huge number of verification tasks, including the semantics of the Java language [21] and the correctness of cryptographic protocols [16]. Most of these proofs use Isabelle/HOL, the version of Isabelle for higher-order logic. Isabelle/HOL's polymorphic type system is ideal for modelling problems in computer science.
Isabelle also supports Zermelo-Fraenkel set theory. Formalized material includes the traditional concepts of functions, ordinals, order types and cardinals. Isabelle/ZF also accepts definitions of recursive functions and data structures; in this it resembles other computational logics, with the important difference of being typeless. Some problems do call for a typeless logic. Isabelle/ZF is also good for investigating foundational issues, and, of course, for formalizing proofs in axiomatic set theory.
Previous published work on Isabelle/ZF describes its basic development [13] and its treatment of recursive functions [13] and inductive definitions [17]. Another paper describes proofs drawn from set theory textbooks [19]. Particularly noteworthy are the proofs of equivalence between various formulations of the axiom of choice. Those proofs, formalized by Grabczewski, are highly technical, demonstrating that advanced set theory proofs can be replicated in Isabelle/ZF given enough time and effort. That is precisely why we should investigate Gödel's proof of the relative consistency of AC: much of the reasoning takes place outside set theory.
The previous section has presented many reasons why we should formalize Gödel's proof directly in the metatheory. That strategy does not require a set theory prover. We could use any system that lets us define the first-order formulae, the set theory axioms, and the set of theorems derivable from any given axioms. We would enjoy a number of advantages.
• Relativization could easily be defined by recursion on the structure of formulae.
• Metatheorems about absoluteness -for example, that all Δ ZF 0 formulae are absolute -could be proved and used to obtain simple proofs of many absoluteness results.
• The constructiveness of the consistency result could be stated and proved.
However, the metatheoretical strategy also presents difficulties. We would have to work in the pure language of set theory, which reduces all concepts to membership and equality, and is unreadable; an alternative would be to formalize the familiar term language. We would constantly be reasoning about an explicitly formalized inference system for ZF rather than using our prover's built-in reasoning tools. I believe this strategy would involve as much work as the strategy I adopted, although the work would be distributed differently.
The choice resembles the standard one we face when we model a formal language: shall we adopt a deep or a shallow embedding? A shallow embedding maps phrases in the language to corresponding phrases in the prover's logic. It works well for reasoning about specific examples, but does not allow metareasoning (proofs about the language). A deep embedding involves formalizing the language's syntax and semantics in the prover's logic. The extra mechanism allows metareasoning but complicates reasoning about specific examples. Compared with a shallow embedding, the strengths and weaknesses are exchanged.
I have chosen to formalize Gödel's theorem in set theory, minimizing any excursions into the metatheory. This strategy still requires defining relational equivalents for each element of set theory's term language, while limiting my exposure to unreadable relational formulae. After all, the critical proofs involve showing that various concepts are absolute, which means that they do not vary from one model of set theory to another. Each absoluteness proof justifies replacing some primitive of the relational language by its counterpart in the term language. Thus Isabelle's simplifier can transform relational formulae into ones using terms, exploiting the existing formalization of set theory.
This plan worked well for basic concepts such as union, intersection, relation, function, domain, range, image, inverse image and even ordinal. The absoluteness proofs for well-orderings, recursive functions and recursive data types were harder: • If a concept is defined in terms of non-absolute primitives, such as powerset, it must be proved equivalent to a suitable alternative definition.
• Much of the theory of well-founded recursion must be formalized from scratch in the relational language.
• Higher-order functions complicate the relational language.
• Recursive functions generate complicated fixedpoint definitions that must be converted into relational form manually.

Relativization and Absoluteness: Basics
The first step is to define the relational language, introducing predicates for all the basic concepts of set theory. Each predicate takes a class as an argument so that it can express relativization. This relational language will later allow appeals to the reflection theorem. Space permits only a few of the predicates to appear below. Note that the class quantifications ∀ ∈ M and ∃ ∈ M are written ∀

From the Empty Set to Functions
We begin with definitions of trivial concepts such as the empty set and the subset relation. A set z is empty if it has no elements: All Isabelle definitions in this paper are indicated by a vertical line, as shown.
A set z is the unordered pair of a and b if it contains those two sets and no others. The Kuratowski definition of ordered pairs , = {{ , }, { , }} is then expressed using the predicate upair: A set z is the union of a and b if it contains their elements and no others. The general union ( ), also written as { | ∈ }, has an analogous definition.
A set z is the domain of the relation r if it consists of each element x such that x,y ∈ r for some y.

Relativizing the Ordinals
Now we can define relational versions of ordinals and related concepts. The formalization is straightforward. An ordinal is a transitive set of transitive sets. A limit ordinal is a non-empty, successor-closed ordinal. A successor ordinal is any ordinal that is neither empty nor limit. The set of natural numbers, , is a limit ordinal that contains no limit ordinals.

Defining the Zermelo-Fraenkel Axioms
Formally defining the ZF axioms relative to a class M lets us express that M satisfies those axioms. Each axiom is relativized so that all quantified variables range over M . We begin with extensionality: The separation axiom is also known as comprehension: This only yields a valid instance of separation if the formula P obeys certain syntactic restrictions. All quantifiers in P must be relativized to M, and the free variables in P must range over elements of M . These restrictions prevent us from assuming separation as a scheme by leaving P as a free variable. We must separately note every instance of separation that we need. If it meets the syntactic restrictions, then later we shall be able to prove that L satisfies it. That looks bad when we recall that the native separation axiom in Isabelle/ZF, and the theorems using it, are schematic in P. But if we formalize Bernays-Gödel set theory as a new Isabelle logic (creating the system Isabelle/BG) then the same problem occurs elsewhere. The analogue of separation in BG set theory is the General Existence Theorem, which is a metatheorem: proving each instance requires a separate construction. To compensate, at least BG has no axiom schemes.
The axioms of unordered pairs, unions and powersets all state that M is closed under the given operation: The foundation axiom states that every non-empty set has a ∈-minimal element: Call a formula univalent over a set if it describes a class function on that set. The replacement axiom holds for univalent formulae: Intuitively, if F is a class function and and is a set, then replacement says that F " (the image of under F ) is a set. However, the axiom formalized above is weaker: it merely asserts (relative to the class M) that F " ⊆ for some set .
To get the set we really want, namely F " , we must apply the axiom of separation to . The weak form of replacement can be proved schematically for L. The strong form cannot be proved schematically because of its reliance on separation.

Introducing a Transitive Class Model
The absoluteness proofs are carried out with respect to an arbitrary class model M, although they are only needed for L. Generalizing the proofs over other models has two advantages: it separates the absoluteness proofs from reasoning about L and it allows the proofs to be used with other class models. Isabelle's locale mechanism [8] makes the generalization possible. A locale packages the many properties required of M, creating a context in which they are implicitly available. A proof within a locale may refer to those properties and to other theorems proved in the same locale. A locale can extend an older one, creating a context that includes everything available in the ancestor locales. The class M is assumed to be transitive (transM ) and to satisfy some relativized ZF axioms, such as unordered pairing (upair ax) and replacement. It contains the set of natural numbers, nat (which is also the ordinal ). This locale does not assume any instances of separation.

Easy Absoluteness Proofs
Here is a canonical example of an absoluteness result. The phrase in M trivial includes the lemma in the locale. The proof refers to the definition of empty set (empty def) and to the transitivity of M (the locale assumption transM ); it uses blast, an automatic prover. The attribute [simp] declares empty abs as a simplification rule: the simplifier will replace any occurrence of empty(M,z) by z=0 provided it can prove M(z). From now on, usually just the statements of theorems will be shown, not header lines and proofs.
Here are some similar absoluteness results, also proved in locale M trivial and declared to the simplifier. Most have trivial proofs like the one shown above. These theorems express absoluteness because the class M disappears from the righthand side: the meaning of subset, image, etc., is the same as its meaning in V. Each theorem also expresses the correctness of an element of the relational language, for example that big union captures the meaning of Union.
Absoluteness results involving ordinals are also easily proved: Thus we see that the simplifier can rewrite relational formulae into term notation, provided we are able to prove that they refer to elements of M . For this purpose, there are many results showing that M is closed under the usual set-theoretic constructions. In particular, we can use the separation axiom for a specific formula P: Also useful are logical equivalences to simplify assertions involving M :

Absoluteness Proofs Assuming Instances of Separation
All the theorems shown above are proved without recourse to the axiom of separation. Obviously many set-theoretic operators are defined using separation -possibly in the guise of strong replacement -so we now extend locale M trivial accordingly. Only a few of the 11 instances of separation appear above. Omitted are the more complicated ones, for example concerning well-founded recursion. By Inter separation it follows that M is closed under intersections. From the lemma declaration, you can see that the proof takes place in locale M basic. All results proved in locale M trivial remain available. By cartprod separation it follows that the class M is closed under Cartesian products. The proof is complicated because the powerset operator (which is not absolute) occurs in the definition. A trivial corollary is that M is closed under disjoint sums. I devoted some effort to minimizing the number of instances of separation required. For example, the inverse image operator is expressed in terms of the image and converse operators. Then the domain and range operators can be expressed in terms of inverse image and image. We obtain five closure theorems from the two assumptions image separation and converse separation: These five operators are also absolute. Here is the result for domain: Although we assume that M satisfies the powerset axiom, we cannot hope to prove M(A) =⇒M(Pow(A)). The powerset of A relative to M is smaller than the true powerset, containing only those subsets of A that belong to M . Similarly, we cannot show that M contains all functions from A to B. However, it holds for a finite case, essentially the set of -tuples: This lemma will be needed later to prove the absoluteness of transitive closure.

Some Remarks About Functions
In set theory, a function is a single-valued relation and thus is a set of ordered pairs. Operators such as powerset and union, which apply to all sets, are not functions. (Strictly speaking, there are no operators in the formal language of set theory, since the only terms are variables.) Isabelle/ZF distinguishes functions from operators syntactically.
• The application of the function f to the argument x is written f'x. On the other hand, application of an operator to its operand is written using parentheses, as in Pow(X), or using infix notation.
• Function abstraction over a set A is indicated by x∈A, and yields a set of pairs. For instance, x∈A. x denotes the identity function on A. Operators are essentially abstractions over the universe, as in x. Pow(Pow(x)). Abstraction can also express predicates; for instance, x. P(x) & Q(x) is the conjunction of the two predicates P and Q.
Kunen [9, p. 14] defines function application in the usual way: ' is "the unique such that , ∈ ." Isabelle/ZF originally adopted a formal version of this definition, using a description operator [13, §7.5]. The relational version of the operator, namely fun apply(M,f,x,y), held if the pair x,y belongs tof for that unique y.
My original definitions of function application, in its infix and relational forms, both followed Kunen's definition. However, the absoluteness theorem relating them was conditional on the function application's being well-defined. That made it harder to simplify fun apply(M,f,x,y) to f'x = y and often forced proofs to include what was essentially type information.
Redefining function application by ' = ( "{ }) solved these problems by eliminating the definite description. The new definition looks peculiar, but it agrees with the old one when the latter is defined. Its relational version is straightforward: Thus it follows that M is closed under function application, which is also absolute:

Well-Founded Recursion
The hardest absoluteness proofs concern recursion. Well-founded recursion is the most general form of recursive function definition. The proof that well-founded relations are absolute consists of several steps. Well-orderings, which are wellfounded linear orderings, are somewhat easier to prove absolute.

Absoluteness of Well-orderings
The concept of well-ordering is the first we encounter whose absoluteness proof is hard. One direction is easy: if relation well-orders , then it also well-orders relative to M. For if every nonempty subset of has an -minimal element, then trivially so does every nonempty subset of that belongs to M; this is Lemma IV 3.14 in Kunen [9, p. 123]. For proving the converse direction, Kunen (Theorem IV 5.4, page 127) reasons that "every well-ordering is isomorphic to an ordinal." We can obtain this result by showing that order types exist in M and are absolute. The proof requires some instances of separation and replacement for M. The theory defines various properties of relations, relative to a class M . Transitivity, linearity, and other simple properties have the obvious definitions and are easily demonstrated to be absolute. The definition of well-founded refers to the existence of r-minimal elements, as discussed above.
A well-ordering is a well-founded relation that is also linear and transitive. Kunen's lemma IV 3.14 takes the following form: The definition of order types is standard; see Theorem I 7.6 of Kunen [9, p. 17]. We use replacement to construct a function that maps elements of A to ordinals, proving that its domain is the whole of A and that each element of its range is an ordinal. Its range is the desired order type. But the construction must be done relative to M . In particular, when we need well-founded induction on r, we must apply a relativized induction rule: One premise is an instance of the separation axiom involving the negation of the induction formula. Each time we apply induction, we must assume another instance of separation.
After about 250 lines of proof script, we arrive at Kunen's Theorem IV 5.4. The notion of well-ordering is absolute: Order types are absolute. That is, if f is an order-isomorphism from between (A,r) and some ordinal i, then i is the order type of (A,r). These results are not required in the sequel, but I found their proofs useful preparation for tackling the more general problem of well-founded recursion.

Functions Defined by Well-founded Recursion Are Absolute
It is essential to show that functions can be defined by well-founded recursion in M and that such functions are absolute. This is Kunen's theorem IV 5.6, page 129. Let be a well-founded relation. If is recursively defined over then ( ) is derived from and from various ( ) where ranges over the set of -predecessors of . This set is just −1 "{ }, the inverse image of { } under , more explicitly { | , ∈ }. Writing the body of as ( , ), with free variables and , we get the recursion equation: Note that ( −1 "{ }) denotes the function obtained by restricting topredecessors of .
If and are given, then the existence of a suitable function follows by well-founded induction over , as I have described in previous work [15]. I have had to repeat some of these proofs relative to M . The theorems may assume only the relativized assumption wellfounded(M,r), which for the moment is weaker than wf(r). About 200 lines of proof script are necessary, but fortunately much of this material is based on earlier proofs. We reach a key result concerning the existence of recursive functions: The predicate is recfun(r,a,H,f) expresses that f satisfies the recursion equation (1) for the given relation r and body H for all r-predecessors of a. So the theorem states that if r is well-founded and transitive then there exists f in M satisfying the recursion equation below a. Obviously r and a must belong to the class M, which moreover must be closed under H. Two additional premises list instances of separation and replacement, which depend upon r and H. Before we can assume such instances, we must express them relative to M . That in turn requires a relativized version of is recfun: This definition is the translation of equation (1) into relational language. (Observe how quickly this language becomes unreadable.) In particular, the binary operator H becomes the ternary relation MH. The argument H makes is recfun a higher-order function, which complicates subsequent work. We cannot relativize is recfun once and for all, but if MH is expressed in relational language, then so is M is recfun.
The predicate relation2 expresses that is f is the relational form of f over M : The predicate is wfrec expresses that z is computed from a and MH by wellfounded recursion over r. The body of the definition expresses the existence of a function f satisfying equation (1) We now reach two lemmas, stating that M is recfun and is wfrec behave as intended. The first result is absoluteness of is recfun. Among the premises are that M is closed under H and that MH is the relational form of H: Under identical premises, we get the corollary "is wfrec(M,MH,r,a,z) ←→ (∃ g [M]. is recfun(r,a,H,g) & z=H(a,g))"

Making Well-founded Recursion Available
Mathematically speaking, we have already proved the absoluteness of wellfounded recursion. Pragmatically speaking, unfortunately, more work must be done to package the results so that they can be used in formal proofs. In particular, we need a theorem relating the predicate is wfrec defined above with the function wfrec provided by Isabelle/ZF [15, §3.1]; wfrec(r,a,H) denotes the result of f(a), where f is the function with body H defined by recursion over r. The development of well-founded recursion assumes r to be transitive. To apply well-founded recursion to other relations requires a theory of transitive closure. Isabelle/ZF defines the transitive closure of a relation inductively [15, §2.5]. Inductive definitions are abstract and elegant, but they do not lend themselves to absoluteness proofs because they use the powerset operator. We must find an alternative definition, and an obvious one is based on the intuition The sequence 0 , 1 , . . . , can be modelled as a finite function: as noted in Section 4.6, finite functions are absolute. From ≺ * it is trivial to define the transitive closure, ≺ + . In the definition below, f is the sequence and A is intended to represent the field of r: It is easy to prove that this definition coincides with Isabelle/ZF's inductive one: "rtrancl alt(field(r),r) = rˆ*" Since every concept used in the new definition is absolute, we merely have to relativize this definition to M, defining rtran closure mem(M,A,r,p) to hold when p is an element of rtrancl alt(A,r). I omit the definition because the relational language is unreadable. We cannot even use the constant 0 but must introduce a variable zero and constrain it by empty(M,zero). The next two predicates relativize the reflexive-transitive and transitive closure of a relation: Once we assume an instance of separation involving rtran closure mem, closure and absoluteness results follow directly: If a relation is well-founded then so is its transitive closure. The following lemma use useful because at this point we do not know that wellfounded(M,r) is equivalent to wf(M,r).
After about 130 lines of proof script, we arrive at some important theorems. One asserts absoluteness, relating the predicate is wfrec with the operator wfrec: The theorems fortunately require identical instances of replacement. Both theorems assume trans(r); omitted are more general theorems that relax the assumption of transitivity. Both theorems use the predicate wfrec replacement to express a necessary instance of replacement. Its arguments are the ternary predicate MH, which represents the body of the recursive function, and the well-founded relation r. 6 Defining First-Order Formulae and the Class L We pause from proving absoluteness results in order to consider our main objective, namely the class L and its properties. The most logical order of presentation might have been to develop L first and then to prove that constructibility is absolute. The order of presentation adopted here better represents how I actually carried out the proofs. Kunen similarly presents general absoluteness results before he introduces L.

Internalized First-Order Formulae
The idea of L is to introduce, at each stage, the sets that can be defined from existing ones by a first-order formula with parameters. Neither Gödel [5] nor Kunen actually use first-order formulae, preferring more abstract constructions that achieve the goal more easily. However, Isabelle/ZF's recursive datatype package automates the task of defining the set of first-order formulae and the satisfaction relation on them. Gödel's earlier proof [6] also uses first-order formulae.
The obvious representation of first-order formulae is de Bruijn's [2], where there are no variable names. Instead, each variable reference is a non-negative integer, where zero refers to the innermost quantifier and larger numbers refer to enclosing quantifiers. If the integer is greater than the number of enclosing quantifiers, than it is a free variable. This representation eliminates the danger of name confusion. It is particularly useful for formulae with parameters, since their order is determined numerically rather than by name.

The Satisfaction Relation
Satisfaction is a primitive recursive function on formulae. Thanks to the nameless representation, interpretations are simply lists rather than functions from variable names to values. The familiar list function nth, defined below, looks up variables in interpretations: "nth(0, Cons(a, l)) = a" "nth(succ(n), Cons(a,l)) = nth(n,l)" "nth(n, Nil) = 0" The second of these equations is subject to the condition n ∈ nat. Note that element zero is the head of the list. Another useful function is bool of o, which converts a truth value to an integer: This conversion is necessary because Isabelle/ZF is based on first-order logic. Formulae are not values, so we encode them using integers. We thus define a recursive predicate as a recursive integer-valued function. We are now able to define the function satisfies, which takes a set (the domain of discourse), a formula and an interpretation (written env for environment). It returns 1 or 0, depending upon whether or not the formula evaluates to true or false: "satisfies(A,Member(x,y)) = ( env ∈ list(A). bool of o (nth(x,env) ∈ nth(y,env)))" "satisfies(A,Equal(x,y)) = ( env ∈ list(A). bool of o (nth(x,env) = nth(y,env)))" "satisfies(A,Nand(p,q)) = ( env ∈ list(A). not ((satisfies(A,p)'env) and (satisfies(A,q)'env)))" "satisfies(A,Forall(p)) = ( env ∈ list(A). bool of o (∀ x∈A. satisfies(A,p)'(Cons(x,env)) = 1))" The abstraction and explicit function applications involving environments are necessary because the environments can vary in the recursive calls. The last line of satisfies deserves attention. The universal formula Forall(p) evaluates to 1 just if p evaluates to 1 in every environment obtainable from env by adding an element of A. Such environments have the form Cons(x,env) for x∈A.
The satisfaction predicate, sats, is a macro that refers to the function satisfies.

The Arity of a Formula
The arity of a formula is, intuitively, its set of free variables. In sats(A,p,env), if the arity of p does not exceed the length of env, then the environment supplies values to all of p's free variables.
Take each de Bruijn reference, adjusted for the depth of quantifier nesting at that point; the arity is the maximum of the resulting values. The recursive definition of function arity is simpler than this description.
"arity(Member(x,y)) = succ(x) ∪ succ(y)" "arity(Equal(x,y)) = succ(x) ∪ succ(y)" "arity(Nand(p,q)) = arity(p) ∪ arity(q)" "arity(Forall(p)) = Arith.pred(arity(p))" Note that ∪ = max{ , } in set theory and that Arith.pred denotes the predecessor function. Trivial corollaries of this definition tell us how to compute the arities of other connectives: "arity(Neg(p)) = arity(p)" "arity(And(p,q)) = arity(p) ∪ arity(q)" The following result is more interesting. Extra items in the environment (exceeding the arity) are ignored. Here @ is the list "append" operator, so env @ extra is env with additional items added. Our aim is to regard the conjunction ∧ as having the free variables , 1 , . . . , . The occurrences of in both formulae must be identified, while the parameter lists of the two formulae must be kept disjoint. To achieve our aim may require renaming one of the formula's free variables.
The de Bruijn representation refers to variables by number rather than by name. The variables shown as above always have the de Bruijn index zero, so they will be identified automatically. We keep the parameter lists disjoint by renumbering the free variables in one of the formulae. Since must be left alone, we only renumber the variables having an index greater than zero.
Renumbering functions are often necessary with the de Bruijn approach, though normally they rename variables during substitution. When efficiency matters, the renumbering functions take an argument specifying what number should be added to the variables. Here, the definitions are for reasoning about rather than for execution, so renaming for us means adding one; repeating this allows renaming by larger integers. In the following definitions, nq refers to the number of quantifiers enclosing the current point. Any de Bruijn index smaller than nq must not be renamed.

The Renaming Function
First, we need a one-line function that renames a de Bruijn variable: "incr var(x,nq) == if x<nq then x else succ(x)" Now we can define the main renaming function. As with satisfies above, abstraction and explicit function applications are necessary: the argument nq ("nesting of quantifiers") varies in the recursive calls. In the Member and Equal case, the variables are simply renamed. The Nand case recursively renames the subformulae using the same nesting depth, while the Forall case renames its subformula using an increased nesting depth.
"incr bv(Member(x,y)) = ( nq ∈ nat. Member (incr var(x,nq), incr var(y,nq)))" "incr bv(Equal(x,y)) = ( nq ∈ nat. Equal (incr var(x,nq), incr var(y,nq)))" "incr bv(Nand(p,q)) = ( nq ∈ nat. Nand (incr bv(p)'nq, incr bv(q)'nq))" "incr bv(Forall(p)) = ( nq ∈ nat. Forall (incr bv(p) ' succ(nq)))" Recall the example at the start of this section, concerning a set defined by the conjunction ∧ . If we are to conjoin the formulae and and combine their sets of parameters, then we need to ensure that some of the parameters are only visible to and the rest are only visible to . The following lemma makes this possible: and thus the renaming allows an additional value to be put into the environment at position m. The renamed formula will ignore the new value. By repeated renaming, we can construct a formula that will ignore a section of the parameter list that is intended for another formula. The next result describes the obvious relationship between arity and renaming. Renaming increases a formula's arity by one, unless the variable being renamed does not exist, when renaming has no effect.
"[[p ∈ formula; n ∈ nat]] =⇒ arity (incr bv(p) ' n) = (if n < arity(p) then succ(arity(p)) else arity(p))" Considering how trivial the notion of arity is, many proofs about it (including this one) are complicated by innumerable case splits. Getting the simplifier to prove most of them automatically requires some ingenuity. Many other tiresome proofs about arities are omitted.

Renaming all but the first bound variable
One more thing is needed before we can define sets using conjunctions. As discussed at the beginning of Sect. 6.4, when a formula defines a set, the variable with de Bruijn index zero gives the extension of that set, while the remaining free variables serve as parameters. Therefore, our basic renaming operator must only rename variables having a de Bruijn index of one or more: "incr bv1(p) == incr bv(p)'1" Finally we reach a lemma justifying our intended use of renaming. If the environment has an initial segment bvs of length n and if we apply the incr bv1 n times, then the modified formula ignores the bvs part. But the renamed and original formulae agree on the first element of the environment, shown above as x.

The Definable Powerset Operation
The definable powerset operator is called DPow: A set X belongs to DPow(A) provided there is an environment env (a list of values drawn from A) and a formula p. The constraint arity(p) ≤ succ(length(env)) indicates that the environment should interpret all but one of p's free variables. The variable whose de Bruijn index is zero determines the extension of X via the satisfaction relation: sats(A, p, Cons(x,env)). You may want to compare this with the informal discussion in the previous section, or with Definition VI 1.1 of Kunen [9, p. 165]. Some consequences of this definition are easy to prove. The empty set is defined by the predicate . ≠ , and singleton sets by . = .
The complement of a set X is defined by negating the formula used to define X. Intersection is done by conjoining the defining formulae, using the renaming techniques developed in the previous section. Union is then trivial by de Morgan's laws.
And thus DPow coincides with Pow (the real powerset operator) for finite sets:

Proving that the Ordinals are Definable
In order to show that DPow is closed under other operations, we must be able to code their defining formulae as elements of the set formula. The treatment of the subset relation is typical. We begin by encoding the formula ∀ . ∈ → ∈ . Below, x and y are de Bruijn indices, which are incremented to succ(x) and succ(x) because the quantifier introduces a new variable binding.
"subset fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))" The arguments are just de Bruijn indices because internalized formulae have no terms other than variables. It is trivial to prove that subset fm maps a pair of de Bruijn indices to a formula: The arity of the formula is the maximum of those of its operands: "[[x ∈ nat; y ∈ nat]] =⇒ arity(subset fm(x,y)) = succ(x) ∪ succ(y)" The following equivalence involves absoluteness, since it relates subset fm to the real subset relation, ⊆. To reach this conclusion requires the additional assumption Transset(A), saying that A is a transitive set. The premise x < length(env) puts a bound on x (which is a de Bruijn index), ensuring that nth(x,env) belongs to A. We must repeat this exercise (details omitted) for the concepts of transitive set and ordinal. This lets us prove that ordinals are definable, leading to a result involving ordinals and DPow. This lemma ultimately leads to a proof that L contains all the ordinals.

Eliminating the Arity Function
The function arity can be surprisingly hard to reason about, particularly when we try to encode higher-order operators. Once we have established the basic properties of L, we can prove its equivalence to a new definition that does not involve arities.
Here is another form of definable powerset:

sats(A, p, Cons(x,env))}}"
This version omits the constraint arity(p) ≤ succ(length(env)) but is otherwise identical to DPow. The point is that if the environment is too short, attempted variable lookups will yield zero; recall the properties of nth from Sect. 6.2. If the set A is transitive, then it contains zero as an element. So the too-short environment can be padded to the right with zeroes.
The following lemma is helpful for proving instances of separation. The first, quantified, premise asks for an equivalence between the real formula P and the internalized formula p. Often we can derive p from P automatically by supplying a set of suitable inference rules.
6.9 The Zermelo-Fraenkel Axioms Hold in L Following Kunen VI §2, it is possible to prove that L satisfies the Zermelo-Fraenkel axioms. Separation is the most difficult case and is considered later.

Basic Properties of L
We begin with simple closure properties. Many of them involve exhibiting an element of formula describing the required set. We typically begin by starting in Lset(i) and proving that the required set belongs to Lset(succ(i)). L is closed under unions: L is closed under unordered pairs. More work is necessary because the sets a and b may be introduced at different ordinals: is closed under ordered pairs provided is a limit ordinal. This result is needed in order to apply the reflection theorem to L. Specifically, it is needed because my version of the reflection theorem [18] uses ordered pairs to cope with the possibility of a formula having any number of free variables.

A Rank Function for L
Some proofs require the L-rank operator. Kunen (VI 1.7) defines ( ) to denote the least such that ∈ +1 : Here is one consequence of this definition: A more important result, whose proof involves lrank, states that every set of constructible sets is included in some Lset: This theorem is useful in proving that L satisfies the separation axiom. However, note that ⊆ L does not imply ∈ L, not even if is a set of natural numbers. The lrank operator is useful for proving that L satisfies the powerset axiom: "L(X) =⇒ L({y ∈ Pow(X). L(y)})" Note that the powerset of X in L comprises all subsets of X that belong to L. It is potentially a superset of DPow(X). The lrank operator also assists in the proof that L satisfies the replacement axiom. The idea is to use replacement on the ranks of the members of L: The proof of replacement is schematic, and therefore independent of the formula Q. But it is the weak form of replacement. It concludes that the range of Q (viewed as a class function) is included in some constructible set Y. Strong replacement, which is the version we really want, asserts that the range itself is constructible. Each instance of strong replacement requires proving an instance of the axiom of separation.

Instantiating the Locale M trivial
Now we are ready to show that L satisfies all the properties we assumed of the class M, which we used to develop the general theory of absoluteness. The class L is transitive: The facts about L proved above can be summarized using the relativized forms of the ZF axioms: "Union ax(L)" "upair ax(L)" "power ax(L)" "replacement(L,P)" We do not need L to satisfy the foundation axiom. However, this fact is a trivial consequence of the foundation axiom: "foundation ax(L)" The theorems above are all we need to prove "PROP M trivial(L)". This theorem makes all the results proved in locale "M trivial" available as theorems about L. In particular, the absoluteness and closure results listed in Sect. 4.5 above apply to L.

Comprehension in L
It remains to show that L satisfies the axiom of separation. The proof requires the reflection theorem. As described elsewhere [18], my formalization of that theorem applies to any class M = ∈ON , where the family { } ∈ON is increasing and continuous. An additional condition is that if is a limit ordinal then must be closed under ordered pairing. Isabelle's locale mechanism captures these requirements, and we can now instantiate the locale with the class L = ∈ON . However, making it ready for practical use requires additional work.

The Reflection Relation
The reflection theorem states that if ( 1 , . . . , ) is a formula in variables then there exists a closed and unbounded class C such that for all ∈ C and 1 ,. . . , In fact, we only need the weaker conclusion that C is unbounded, which enables us to find a suitable > given any ordinal . Applying the reflection theorem yields an Isabelle formula describing the class C. These formulae may be interesting in the case of small examples [18], but in typical applications they are huge. The trivial proofs, which merely refer to other instances of reflection, take minutes of computer time; the resulting theorems amount to pages of text. The obvious solution is to express the reflection theorem using an existential quantifier, but classes cannot be quantified over: they are formulae.
Fortunately, Isabelle makes a distinction between the object-logic (here firstorder logic) and the metalogic (a fragment of higher-order logic) [12]. I was able to formalize a metaexistential quantifier. It lies outside of first-order logic -in particular, Isabelle will reject any attempt to use it in comprehensions. However, it can be used in top-level assertions, which is all we need. We can now define the reflection relation between two formulae P and Q: Q(a,x))))" It relates the formulae just if there exists a class C satisfying the conclusion of the reflection theorem [18]. That is, C is a closed, unbounded class of ordinals such that P and Q agree on . The existential quantifier, ??C, hides the prohibitively large formula describing this class. The following lemma illustrates the use of the reflection relation. Note that the quantification over classes has disappeared.
If REFLECTS[P,Q] and i is an ordinal then there exists a larger ordinal j for which P and Q agree. Our choice of i can make j arbitrarily large.
The general form of the reflection theorem uses the relativization operator, which cannot be expressed in Isabelle/ZF. However, given a specific formula , we can generate an instance of the reflection theorem relating L and . Here is the base case, where normally P should have the form ∈ or = : In the conclusion, a quantification over L is related to one over , as suggested by the general form of the reflection theorem. The premise uses the projection operators for ordered pairs to introduce the new variable, z; syntactically, x. P(fst(x),snd(x)) is a unary formula.

Internalized Formulae for Some Set-Theoretic Concepts
Every operator or concept that is used in an instance of the axiom of separation must be internalized. If the defining formula is complicated, then writing the corresponding element of formula requires a manual (and error-prone) translation into de Bruijn notation. The Isabelle/ZF development of constructibility theory contains about 100 such encodings. A typical example resembles that shown in Sect. 6.6 above for subset fm. First to be internalized are elementary concepts such as the empty set, unordered and ordered pairs, unions, intersections, domain and range.
The union predicate was defined in Sect. 4.1 as In the corresponding formula, the variables x, y and z range over de Bruijn indices.
"union fm(x,y,z) == Forall(Iff(Member(0,succ(z)), Or(Member(0,succ(x)), Member(0,succ(y)))))" As for subset fm above, we can prove that union fm yields an element of the set formula. The theorem about satisfaction now takes the following form: "[[x ∈ nat; y ∈ nat; z ∈ nat; env ∈ list(A)]] =⇒ sats(A, union fm(x,y,z), env) ←→ union( ** A, nth(x,env), nth(y,env), nth(z,env))" Here, ** A is Isabelle syntax for the class given by the set A, that is, { | ∈ }. The theorem above simply expresses the equivalence between the relational formula union and union fm, which is its translation into an element of set formula. Such equivalences are usually trivial: they simply relate two syntaxes for formulae. They do not express the equivalence between union fm and ∪, which would be an instance of absoluteness.
After internalizing a predicate such as union, it makes sense to prove its instance of the reflection theorem too, since both results will be needed when proving instances of separation. Most reflection proofs are trivial two-line scripts: 1. Unfold the concept's definition (here union).

Repeatedly apply existing reflection theorems.
Each predicate is internalized similarly. Parts of the declarations and proofs can be copied from those of another predicate. However, getting the definition right requires careful attention to the original first-order definition.

Higher-Order Syntax
Higher-order syntax is ubiquitous in naive set theory.In the union ∈ ( ), the higher-order variable represents an indexed family of sets. In the function abstraction ∈ ( ), the higher-order variable represents the function's body. Isabelle/ZF additionally uses higher-order syntax to express many forms of recursion, and so forth. Although this syntax is indispensable, it is also illegitimate: formal set theory has no non-trivial terms, let alone higher-order ones. We must formalize the conventions governing higher-order syntax into the language of set theory.
Converting a higher-order operator such as x∈A. b(x) into relational form yields a higher-order predicate. Among its arguments is a predicate is b that expresses the function body, b, in relational form. If is b is purely relational, then so is the definiens of is lambda.
This definition states that z is a -abstraction provided its elements are ordered pairs that satisfy is b and whose first component belongs to A.
The following predicate expresses that is f represents the relational version of f for arguments ranging over A: This abbreviation, and similarly Relation2, etc., are useful for expressing absoluteness results. If is b is the relational equivalent of b, and if the class M contains each b(m) for m∈A, then is lambda(M,A,is b,z) is the relational version of x∈A. b(x). And thus -abstraction is absolute: Showing that M is closed under -abstraction requires a separate instance of strong replacement for each b. Internalizing is lambda is not completely straightforward. The predicate argument, is b, becomes a variable ranging over the set formula.
"lambda fm(p,A,z) == Forall(Iff(Member(0,succ(z)), Exists(Exists(And (Member(1,A#+3), And(pair fm(1,0,2), p))))))" Given a formula and two de Bruijn indices, lambda fm yields another formula: But there is no binding mechanism for expressing predicates that take arguments or refer to local variables. The formula p must refer to its first argument using the de Bruijn index 1 and to its second using the index 0 (both to be increased in the usual way if p contains quantifiers). If we are lucky, then we can arrange matters such that the actual arguments have the right indices, and otherwise we can force the indices to agree by introducing quantifiers and equalities: in the internalization of ∀ . ∀ . = ∧ = → , the variable with de Bruijn index 1 will refer to and similarly the index 0 will refer to . If p contains free references to other variables, their de Bruijn indices must be increased by 3 because p is inserted into a context enclosed by three quantifiers. The satisfaction theorem for is lambda formalizes the remarks above: lemma sats lambda fm: assumes is b iff sats ∈ "!!a0 a1 a2.
[[a0∈A; a1∈A; a2∈A]] =⇒ is b(a1,a0) ←→ sats(A, p, Cons(a0,Cons(a1,Cons(a2,env))))" shows "[[x ∈ nat; y ∈ nat; env ∈ list(A)]] =⇒ sats(A, lambda fm(p,x,y), env) ←→ is lambda( ** A, nth(x,env), is b, nth(y,env))" The assumes-shows syntax eases the use of the complicated assumption, which states that is b agrees with p for the fixed environment env extended with three additional elements of A. I have not been able to simplify the form of this theorem while retaining its generality. It gets more complicated when one higher-order operator refers to another. One such operator has a quantifier nesting depth of 12. When an operator uses its higher-order argument more than once, we must ensure that the two contexts are similar, adding quantifiers if necessary to make the nesting depths agree.
Instances of the reflection theorem for higher-order operators must take into account the possibility of the higher-order argument's referring to local variables. Although is lambda expects is b to have only two arguments, below we formalize it with three arguments (plus its class argument). The extra argument is bound by the REFLECTS operator, allowing direct reference to elements of L or Lset(i).
theorem is lambda reflection: assumes is b reflection: The arity of a higher-order function naturally depends upon that its function argument. I found the properties so unintuitive and their proofs so vexing that I undertook the work described in Sect. sec:no-arity, which eliminates the need for theorems concerning arities.

Proving Instances of Separation
The set comprehension { ∈ | ( )} comes from the separation axiom scheme instantiated to the formula . The axiom of replacement yields a set that may be bigger than we want, again requiring an appeal to separation. Because I have not formalized the metatheory, the Isabelle/ZF development cannot express the proof that the separation scheme holds for L. Each instance has to be proved individually. Fortunately, the proof scripts are nearly identical. Given , the first step is to prove instance of the reflection theorem for that formula. The next step is to run a proof script corresponding to the sketch in Kunen [9, p. 169]. The formula will of course be expressed using the relational language, using predicates such as union. Executing the proof script will automatically generate an internalized formula, with union fm in the corresponding place.
The lemmas outlined on the preceding pages suffice to prove many instances of separation. Consider the instance that justifies the existence of the intersection Inter(A). We must first prove the corresponding instance of the reflection theorem: Such instances are written manually. A text editor can replace quantification over L by quantification over in the second formula. The proof, almost always, is a one-line appeal to previous reflection theorems.
The statement of each instance of separation comes from the corresponding locale assumption. The locale refers to an arbitrary class M, so we must replace M by L. The proof scripts are typically three lines long and follow a regular pattern. Note that any parameters used in the separation formula (here ) must be elements of L. The following instance of separation justifies relational composition. I leave the corresponding instance of reflection to your imagination. After proving ten or so instances of separation, we arrive at a cryptic theorem: This asserts that L satisfies the conditions of the locale M basic, namely all the instances of separation needed to derive well-founded recursion. The absoluteness and closure results proved in that locale (described in Sect. 4.6) -now become applicable to L.

Automatic Internalization of Formulae
Isabelle's ability to translate formulae written in the relational language into members of formula simplifies the proofs of separation. Here is an example, from the proof of the instance shown above (about relational composition). The first proof step applies a lemma for proving instances of separations. It yields a subgoal that has the assumptions r ∈ Lset(j) and s ∈ Lset(j), where j is arbitrary. We have to prove that the comprehension belongs to the next level of the constructible hierarchy, namely DPow(Lset(j)): The second proof step applies a lemma for proving membership in DPow(Lset(j)). It yields three subgoals (Fig. 2). The first is to show the equivalence between the real formula (∃ xa∈Lset(j). ∃ y ∈Lset(j). ...) and sats(Lset(j), ?p3(j), [x,r,s]). This is the satisfaction relation applied to ?p3(j), a "logical variable" that can be replaced by any expression, possibly involving the bound variable j. The third subgoal in Fig. 2, namely ?p3(j) ∈ formula, checks that the chosen expression is an internalized formula. The second subgoal verifies that the environment, [r,s], is well-typed -namely, that it belongs to list(Lset(j)).
The third proof step is this: apply (rule sep rules | simp)+ It applies some theorem of sep rules, then simplifies, then repeats if possible. This finishes the proof. All separation proofs have this form, save only that sometimes sep rules needs to be augmented with additional theorems. Formula synthesis works in a way familiar to all Prolog programmers. Essentially, the theorems in sep rules comprise a Prolog program for generating internalized formulae. Most of the "program clauses" relate real formulae to internal ones and are derived from the basic properties of the satisfaction relation. For example, this one relates the real conjunction P&Q with the term And(p,q). The first two subgoals concern the synthesis of p and q. The third subgoal expresses a type constraint on env. 1. j x. [[L(r); L(s); r ∈ Lset(j); s ∈ Lset(j); x ∈ Lset(j)]] =⇒ (∃ xa∈Lset(j). ∃ y ∈Lset(j). ∃ z∈Lset(j). pair( ** Lset(j), xa, z, x) ∧ (∃ xy ∈Lset(j). pair( ** Lset(j), xa, y, xy) ∧ (∃ yz∈Lset(j). pair( ** Lset(j), y, z, yz) ∧ xy ∈ s ∧ yz ∈ r))) ←→ sats(Lset  The environment, which initially contains the parameters of the separation formula, gets longer with each nested quantifier. Each higher-order operator can add several elements to the environment; as mentioned above in Sect. 7.3. A base case of synthesis relates the formula x∈y with the term Member(i,j). The first two subgoals concern the synthesis of the de Bruijn indices i and j: Other base cases concern predicates of the relational language. This theorem, which relates the formula union( ** A,x,y,z) with the term union fm(i,j,k), is just a reworking of a theorem shown in Sect. 7.2 above.
"[[nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; i ∈ nat; j ∈ nat; k ∈ nat; env ∈ list(A)]] =⇒ union( ** A, x, y, z) ←→ sats(A, union fm(i,j,k), env)" Given the subgoal nth(?i,env) = x, Isabelle can synthesize ?i. This de Bruijn index is determined by x, which comes from the original formula, and env, which is given in advance. If x matches the head of the environment, then ?i should be zero: "nth(0, Cons(a, l)) = a" And if it does not match, then we should discard the head and attempt to synthesize a de Bruijn index using the tail: "[[nth(n,l) = x; n ∈ nat]] =⇒ nth(succ(n), Cons(a,l)) = x" The automatic synthesis of internalized formulae saves much work in proofs of separation. In principle, we could rewrite every relational formula into its primitive constituents of membership and equality, removing the need for union fm and 100 similar constants. But if too few internalized primitives have been defined, formula synthesis takes many minutes.

Absoluteness of Recursive Datatypes
The Isabelle/ZF proofs discussed up to now include the construction of the class L and the proof that it is a model of the Zermelo-Fraenkel axioms. The next step is to show that L satisfies V = L. That fact follows by the absoluteness of constructibility, which follows by the absoluteness of satisfaction. Consulting the definition of satisfies reveals that we must still prove the absoluteness of lists, formulae, the function nth, and several other notions.
Isabelle/ZF defines the sets list(A) and formula automatically from their user-supplied descriptions [17]. These fixedpoint definitions have advantages, but their use of the powerset operator is an obstacle to proving absoluteness. For a start, Pow(D) must be eliminated from this definition:  We can prove that the least fixedpoint of a monotonic, continuous function h can be expressed as the union of the finite iterations of h.
This equation not only eliminates Pow(D), but every occurrence of D, which is the "bounding set" [15, §2.2] and is itself typically defined using powersets.
In order to apply this equation, we must prove that standard datatype constructions preserve continuity. The case bases are that the constant function and the identity function are continuous: "contin( X. A)" "contin( X. X)" Sums and products preserve continuity: These four lemmas cover all finitely-branching datatypes, including lists and formulae.

Absoluteness for Function Iteration
In the equation above for least fixed points, the term hˆn(0) abbreviates iterates(h,n,0). Isabelle/ZF defines iterates(F,n,x) by the obvious primitive recursion on n∈nat. Absoluteness of datatype definitions will follow from the absoluteness of iterates.
Recall that a well-founded function definition consists of a relation and function body ; recall equation (1) of Sect. 5.2. Relativizing such a function definition, requires relativizing by an Isabelle/ZF relation, say MH. So to relativize iterates, we declare is iterates in terms of another predicate iterates MH, representing the body of the recursion. Incidentally, is nat case(M,a,isb,n,z) expresses case analysis on the natural number n. Note that we again work in the general setting of a class M satisfying certain conditions. Later, we shall prove that L meets those conditions. The absoluteness theorem for well-founded recursion requires an instance of strong replacement for each function being defined. But iterates is a higherorder function, so technically iterates(F,n,x) involves a separate instance of well-founded recursion for each F. The function iterates replacement can express each required instance of replacement; its argument isF is the relational form of F. Assuming such an instance of replacement, and given that isF is the relational version of F, the absoluteness of iterates is a corollary of the general theorem about well-founded recursion. We similarly find that M is closed under function iteration.

Absoluteness for Lists and Formulae
The formal treatment of continuity and iterates enables us to prove that lists and formulae are absolute. The definition of lists generated by the Isabelle/ZF datatype [17] is too complicated to relativize easily. Instead, we prove its equivalence to a more abstract (and familiar) definition. The function given to lfp continuous by construction, which lets us replace the the least fixed point by iteration and eliminate the non-absolute set univ(A): "contin( X. {0} + A * X)" "list(A) = ( n∈nat. ( X. {0} + A * X)ˆn (0))" Now the absoluteness of list(A) is obvious. But each element of this equation must be formalized in order to prove absoluteness. We begin by introducing an abbreviation for finite iterations of X. {0} + A * X -that is, for finite stages of the list construction.  Formulae are proved absolute in just the same way. We express the set formula as an abstract least fixed point of a suitable function, prove that function to be continuous, and eliminate the lfp operator: "formula = lfp(univ(0), X. ((nat * nat) + (nat * nat)) + (X * X + X))" "contin( X. ((nat * nat) + (nat * nat)) + (X * X + X))" "formula = ( n∈nat. ( X. ((nat * nat) + (nat * nat)) + (X * X + X))ˆn (0))" Proceeding as for lists, we define the predicates is formula functor, is formula N, mem formula and finally is formula. We obtain the desired theorems:

Recursion over Lists and Formulae
We have already seen (Sect. 5) that functions defined by well-founded recursion are absolute. For mathematicians, that is enough to justify the absoluteness of functions defined recursively on lists or formulae. Proof tool users, however, must work through the details for each instance. Usually automation makes it easy to apply general results to particular circumstances. However, the Isabelle/ZF translation of recursive function definitions is rather complicated. 3 There are good reasons for this complexity, such as support for a form of polymorphism. However, it makes the absoluteness proofs more difficult: the complications have to be taken apart and relativized one by one. At least there is no need to treat recursion over lists. Defining the class L involves only one list function, namely nth. Given a natural number and a list , this function returns the th element of , counting from 0. Obviously this amounts to taking the tail of the list times and returning the head of the result. The recursion in nth is an instance of iterates.
Isabelle/ZF defines the head and tail functions hd and tl. The absoluteness proofs use modified versions called hd' and tl', which extend hd and tl to return 0 if their argument is ill-formed (the details are unimportant). Relativization is simpler when a function's behaviour is fully specified. Now we can prove an equivalence for nth: "[[xs ∈ list(A); n ∈ nat]] =⇒ nth(n,xs) = hd' (tl'ˆn (xs))" Its relational equivalent, is nth, has an obvious definition in terms of the relational equivalents of iterates, tl and hd: Recursion over lists is absolute in general. Proving this claim would require much work, and is unnecessary for proving that V = L is absolute. The function satisfies involves recursion over the datatype of formulae, and its absoluteness proof consists of several stages. Isabelle/ZF expresses recursion on datatypes in terms of ∈-recursion, which is recursion on a set's rank [15, §3.4]. Absoluteness for ∈-recursion will follow from that of well-founded recursion once we have established the absoluteness of ∈-closure. Then we shall be in a position to consider recursion over formulae.
Five instances of strong replacement are necessary for the proofs sketched above. There are two each for the absoluteness of list(A) and formula, and one for the absoluteness of nth(n,l). The locale M datatypes encapsulates these additional constraints on the class M . It is one of several locales used to keep track of instances of separation and replacement in this development.

Absoluteness for ∈-Closure
If is a set, then its ∈-closure is the smallest transitive set that includes . Formally, the ∈-closure of is ∈ ( ). Here ( ) denotes the -fold union of , defined by 0 ( ) = and +1 ( ) = ( ( )). This is just another instance of iterates, as we can prove:
Its definition is a straightforward combination of the operators eclose, wfrec (which expresses well-founded recursion), and Memrel (which encodes the membership relation as a set). Thus the definition of the relational version, is transrec, is also straightforward. Our previous results lead directly to a proof of absoluteness: In these theorems, transrec replacement abbreviates a specific use of wfrec replacement, which justifies this particular recursive definition (recall Sect. 5.3).

Recursion over Formulae
The Isabelle/ZF treatment of recursive functions on datatypes involves nonabsolute concepts, namely the cumulative hierarchy { } ∈ON and the rank function [15, §3.6]. For proving absoluteness, I proved an equation stating that recursion over formulae could be expressed differently. The new formulation refers to the depth of a formula, defined by "depth(Member(x,y)) = 0" "depth(Equal(x,y)) = 0" "depth(Nand(p,q)) = succ(depth(p) ∪ depth(q))" "depth(Forall(p)) = succ(depth(p))" Introducing depth seems to be a step backwards, since it requires relativizing another recursive function on formulae. But we can express the depth of a formula in terms of is formula N, which we need anyway (Sect. 8.2); is formula N(M,n,F) holds just if F is the set of formulae generated by n unfoldings of the datatype definition -which is all formulae of depth less than n. Working from this definition, we find that the depth of a formula is absolute: "[[p ∈ formula; n ∈ nat]] =⇒ is depth(M,p,n) ←→ n = depth(p)" For relativization, I modified the standard Isabelle/ZF treatment of recursion over formulae, replacing the set by formula and the rank of a set by the depth of a formula. If f is a recursive function on formulae, then the evaluation of f(p) begins by determining the depth of p, say . Then the recursion equation for f is unfolded + 1 times, using transfinite recursion. The resulting nonrecursive function is finally applied to p. This approach unfortunately needs an explicitabstraction over formulae and another instance of the replacement axiom. With the benefit of hindsight, I might have saved much work by seeking simpler ways of expressing recursion over formulae, such as by well-founded recursion on the subformula relation.
The recursive definition of a function f is specified by four parameters a, b, c and d, corresponding to the four desired recursion equations: Given the datatype definition of formula, Isabelle/ZF automatically defines the operator formula rec for expressing recursive functions. The term formula rec(a,b,c,d,p) denotes the value of the function f above applied to the argument p. More concisely, formula rec(a,b,c,d) denotes the the function f itself. The details of the definitions are illustrated elsewhere, using the example of lists [15, §4.3].
In order to express the recursion theorem, it helps to have first defined an abbreviation for its case analysis on formulae.
Now we can express recursion on formulae in terms of absolute concepts: formula rec(a,b,c,d,p) = transrec (succ(depth(p)), x h. Lambda(formula, formula rec case(a,b,c,d,h))) ' p" The proof is by structural induction on p. Note that the argument h of formula rec case is a partially unfolded recursive function taking two curried arguments. The second argument is some subformula u and the first is succ(depth(u)). The intuition behind this theorem may be obscure, but that is no obstacle to proving absoluteness. Many routine details must be taken care of, including relativization and absoluteness for the formula constructors Member, Equal, Nand and Forall and for the operator formula case.
Obviously formula rec is a higher-order function. Its absoluteness proof depends upon absoluteness assumptions for the function arguments a, b, c and d. Its relational version needs those arguments to be expressed in relational form as predicates is a, is b, is c and is d. The absoluteness theorem depends upon 10 assumptions in all: two for each of is a, is b, is c and is d and two instances of replacement. After many intricate but uninteresting details, we arrive at two key theorems. If the class M is closed under the parameters a, b, c and d then it is closed under the corresponding recursion: Recursion over formulae is absolute: =⇒ is formula rec(M,MH,p,z) ←→ z = formula rec(a,b,c,d,p)" In this theorem, MH abbreviates the relativization of the argument of transrec shown above: 9 Absoluteness for L In order to prove V = L, we must prove the absoluteness of three main functions: 1. satisfies, the satisfaction function on formulae 2. DPow, the definable powerset function 3. Lset, which expresses the levels of the constructible hierarchy.
Of these functions, Lset is defined by transfinite recursion from DPow, which in turn has a straightforward definition in terms of satisfies. But proving the absoluteness of satisfies is very complicated. Absoluteness of satisfies is merely an instance of the absoluteness of recursion over formulae, and is therefore trivial. That does not relieve us of the task of formalizing the details. The file containing the satisfies absoluteness proof is one of the largest in the entire development. This file divides into two roughly equal parts.
The first half contains internalizations and reflection theorems for operators such as depth and formula case. It expresses the four cases of satisfies in both functional and relational form, and proves absoluteness for each case. Six instances of strong replacement are required: one for each case of the recursion (because each contains a -abstraction), another to justify the use of transrec, and yet another to justify the -abstraction in formula rec. These axioms are assumed to hold of an arbitrary class model M . They are used to show that the formalization satisfies the conditions of the absoluteness theorem for formula rec described in the previous section.
The second half of the file is devoted to proving that the six instances of replacement hold in L. The four cases of the recursion (in their relational form) must each be internalized. This tiresome task involves, as always, translating a definition involving real formulae into one using internalized formulae. Then, the six instances of replacement are justified. Finally, the pieces are put together.
In order to relativize satisfies, we must first define constants corresponding to formula rec's parameters a, b, c and d. Here are the two base cases: Each of these functions is then re-expressed in relational form. Here is the first: Once we have done the other three, we can define an instance of MH for satisfies, expressing the body of the recursion as a predicate: At this point we must assume (by declaring a locale) the six instances of replacement mentioned above. That enables us to prove absoluteness for the parameters a, b, c and d used to define satisfies. For example, the class M is closed under satisfies a: This theorem states that satisfies is a(M,A,x,y,zz) is the relational equivalent of satisfies a(A,x,y) provided x and y belong to the set nat. It can be seen as an absoluteness result subject to typing conditions on x and y. Proofs are obviously easier if the absoluteness results are unconditional, but sometimes typing conditions are difficult to avoid. Analogous theorems are proved for satisfies is b, satisfies is c and satisfies is d. Thus we use the first four instances of replacement. The last two instances, which are specific to satisfies, let us discharge the more general instances of replacement that are conditions of formula rec's absoluteness theorem. We ultimately obtain absoluteness for satisfies:

Proving the Instances of Replacement for L
Now we must justify those six instances of strong replacement by proving that they hold in L. Recall that strong replacement is the conjunction of replacement (which holds schematically in L, but may yield too big a set) and an appropriate instance of separation (Sect. 4.3).
As always, proving instances of separation requires internalizing many formulae. Isabelle can do this automatically, but unless it is given enough internalized formulae to use as building blocks, the translation requires much time and space. I internalized many concepts manually, declaring their internal counterparts as constants and proving their correspondence with the original concepts. Here is the internal equivalent of satisfies is a: "satisfies is a fm(A,x,y,z) == Forall( Implies(is list fm(succ(A),0), lambda fm( bool of o fm(Exists( Exists(And(nth fm(x#+6,3,1), And(nth fm(y#+6,3,0), Member(1,0))))), 0), 0, succ(z))))" Obviously, the same task must be done for the other satisfies relations and for the concepts used in their definitions. We finally can internalize the body of satisfies: "satisfies MH fm(A,u,f,zz) == Forall( Implies(is formula fm(0), lambda fm( formula case fm(satisfies is a fm(A#+7,2,1,0), satisfies is b fm (A#+7,2,1,0), satisfies is c fm(A#+7,f#+7,2,1,0), satisfies is d fm(A#+6,f#+6,1,0), 1, 0), 0, succ(zz))))" Now, we can prove the six instances of replacement. Here is the first one, for the Member case of satisfies: The theorem statement may look big, but the proof has only four commands. The corresponding instances of the reflection theorem (not shown) is twice as big, but its proof has only one command. We proceed to prove the fifth instance of replacement: Our reward for this huge effort is that the absoluteness of satisfies now holds for L: =⇒ is satisfies(L,A,p,z) ←→ z = satisfies(A,p)"

Absoluteness of the Definable Powerset
Conceptually, the absoluteness of DPow is trivial, since it is just a comprehension involving satisfies. The formal details require a modest effort. There are more internalizations, such as that of is formula rec. Note that concepts only have to be internalized if they appear in an instance of separation, which may only happen long after the concept is first relativized. Unfortunately, formula rec is a complex higher-order function; in its relational form, one argument gets enclosed within 11 quantifiers. Completing this task enables us to internalize is satisfies: "satisfies fm(x) == formula rec fm(satisfies MH fm(x#+5#+6,2,1,0))" Recall that DPow is the definable powerset operator. It has a variant form, DPow', that does not involve the function arity. The two operators agree on transitive sets, so in particular we can use DPow' to construct L. Now we must relativize DPow'. Its definition refers to the powerset operator, which is not absolute. It can equivalently be expressed using a set comprehension, which here represents an appeal to the replacement axiom: Within the comprehension is another comprehension, which appeals to separation. The formula sats(A, p, Cons(x,env)) needs to be relativized (as the predicate is DPow sats) and internalized. Then, we again extend the list of assumptions about the class M to include these instances of replacement and separation. Using them, we can prove that M is closed under definable powersets: We can also express the equation for DPow' shown above in relational form, defining the predicate is DPow', and prove absoluteness: To make these results available for L, we must first prove that L satisfies the new instances of replacement and separation. Here is the latter: =⇒ separation(L, x. is DPow sats(L,A,env,p,x))"

Absoluteness of Constructibility
The proof that L satisfies V = L nearly finished. Only the operator Lset, which denotes the levels of the constructible hierarchy, remains to be proved absolute.
Recall that it can be expressed using DPow': "Lset(i) = transrec(i, %x f. y ∈x. DPow' (f ' y))" So now we must internalize the predicate is DPow'. First we must internalize the operators used in its definition. Among those are the predicate is Collect, which recognizes set comprehensions. The equation for Lset above involves two further instances of replacement: one for the use of transrec and another for the indexed union. Adding them to our list of constraints on M allows us to prove that that class is closed under the Lset operator: We can also define its relational version: "is Lset(M,a,z) == is transrec(M, %x f u. u = ( y ∈x. DPow' (f ' y)), a, z)" Notice that this definition is not purely relational. That is all right because is Lset is not used in any instance of separation and thus need not be internalized. We can now prove that the constructible hierarchy is absolute: As remarked earlier, results such as this express absoluteness because the class model M drops out of the right-hand side. The left-hand side refers to our formalization of in M, which by the theorem is equivalent to itself. As always, making this result available to L requires proving the new instances of replacement. I omit the details, which contain nothing instructive.
We can finally formalize L M , the relativization of L. A set x is constructible (with respect to any class M satisfying the specified ZF axioms) provided there exists an ordinal i and a level of the constructible hierarchy Li such that x ∈ Li. The following theorem is a trivial consequence of the absoluteness results and the definitions of constructible and L. "L(x) =⇒ constructible(L,x)" This theorem expresses our goal, namely that V = L holds in L or more formally (V = L) L . For this statement is equivalent to (∀ . L( )) L and thus to ∀ . L( ) → L L ( ). We can drop the universal quantifier. The antecedent of the implication is formalized as L(x) and the consequent as constructible(L,x). This proof ends the most difficult part of the development.

The Axiom of Choice in L
The formalization confirms that V = L is consistent with the axioms of set theory. Obviously any consequence of V = L, such as the axiom of choice, is consistent with those axioms too. Proving consequences of V = L involves working in an entirely different way, and a much pleasanter one. Dispensing with the relational language, relativization, internalization and absoluteness, we can instead work in native set theory with the additional axiom V = L.
Assuming V = L, the proof of the axiom of choice is simple [9, p. 173]. It suffices to prove that every set can be well-ordered. In fact, we can well-order the whole of L. The set of internalized formulae is countable, and therefore wellordered. The well-ordering of L derives from its cumulative construction and from the well-ordering of formulae. For , ∈ L, say that precedes if • originates earlier than in the constructible hierarchy -that is, there is some such that ∈ and ∉ .
• and originate at the same level , but the combination of defining formula and parameters for lexicographically precedes the corresponding combination for .
Each element of +1 is a subset of that can be defined by a formula, possibly involving parameters from . We can assume the induction hypothesis that is well-ordered. Before we can undertake this transfinite induction, we must complete several tasks: 1. exhibiting a well-ordering on lists, for the parameters of a definable subset 2. exhibiting a well-ordering on formulae 3. combining these to obtain a well-ordering of the definable powerset 4. show how to extend our well-ordering to the limit case of the transfinite induction

A Well-Ordering for Lists
First we inductively define a relation on lists: the lexicographic extension of a relation on the list's elements. Let r denote a relation over the set A. Then the relation rlist(A,r) is the least set closed under the following rules: There are several well-known injections from × into , but defining one of them and proving it to be injective would involve some effort. Instead we can appeal to a corollary of ⊗ = , which is already available [19, §5] in Isabelle/ZF: Thus we have × ≈ : there is a bijection, which is also an injection, between × and . However, although an injection exists, we have no means of naming a specific bijection. Therefore, we conduct the entire proof of the axiom of choice under the assumption that some injection exists. The final theorem is existential, which will allow the assumption to be discharged.
We declare a locale to express this new assumption, calling the injection fn. Recall that nat is Isabelle/ZF's name for the ordinal : locale Nat Times Nat = fixes fn assumes fn inj: "fn ∈ inj(nat * nat, nat)" Proving that enum(fn,p) defines an injection from formulae into the naturals requires a straightforward double induction over formulae: "( p ∈ formula. enum(fn,p)) ∈ inj(formula, nat)" Using the enumeration as a measure function, we find that the set of formulae is well-ordered: "well ord(formula, measure(formula, enum(fn)))" The functions defined below all have an argument f, which should range over injections from × into . In proofs, this injection will always be fn from locale Nat Times Nat. The definiens of a constant definition cannot refer to fn because it is a variable.

Defining the Well-ordering on DPow(A)
The set DPow(A) consists of those subsets of A that can be defined by a formula, possibly using elements of A as parameters (Sect. 6.5). We can define a wellordering on DPow(A) from one on A. We get a well-ordering on formulae from their injection into the natural numbers. To handle the parameters, we define a wellordering for environments -lists over A -and combine it with the well-ordering of formulae. A subset of A might be definable in more than one way; to make a unique choice, we map environment/formula pairs to ordinals. The well-ordering on environment/formula pairs is the lexicographic product (given by rmult) of the well-orderings on lists (rlist) and formulae (measure).

Well-Ordering in the Limit Case
The proof that is well-ordered appeals to transfinite induction on the ordinal . The induction hypothesis is that is well-ordered if < . In the limit case, = < . Recall (Sect. 6.9.2) that L-rank ( ) of is the least such that ∈ +1 . If is a limit ordinal then we order elements of first by their L-ranks; if two elements have the same L-rank, say , then we order them using the existing well-ordering of +1 .

Transfinite Definition of the Well-Ordering for L
The well-ordering on L is defined by transfinite recursion. The Isabelle definition refers to the cryptic transrec operator, so let us pass directly to the three immediate consequences of that definition. For the base case, the well-ordering is the empty relation: "L r(f,0) = 0" For the successor case, the well-ordering is given by applying DPow r to the previous level.
"Limit(i) =⇒ L r(f,i) = rlimit(i, L r(f))" Thanks to the results proved above, a simple transfinite induction proves that L r(fn,i) well-orders the constructible level Lset(i).
"Ord(i) =⇒ well ord(Lset(i), L r(fn,i))" Note that this theorem refers to fn, an injection from × into . Recall (Sect. 10.2) that we know such that such functions exist but have not defined a specific one. We have been able to prove our theorems by working in a locale that assumes the existence of fn. Now, we can eliminate the assumption. We use an existential quantifier to hide the well-ordering in the previous theorem, so that fn no longer appears. Then, by the mere existence of such an injection, it follows that every Lset(i) can be well-ordered: "Ord(i) =⇒ ∃ r. well ord(Lset(i), r)" To wrap things up, let us package the axiom V = L as a locale: locale V equals L = assumes VL: "L(x)" The axiom of choice -in the guise of the well-ordering theorem -is a trivial consequence of the previous results.

Conclusions
What has been accomplished? I have mechanized the proof of the relative consistency of the axiom of choice, largely following a standard textbook presentation. The formal proof is much longer than the textbook version because it is complete in all details and uses no metatheoretical reasoning. As noted in Section 2, Gödel's proof comprises four tasks, which we can now express more precisely: The proof that L satisfies V = L is by far the largest and most difficult part of the development. It involves proving L to be absolute, which requires converting every concept used in its definition into relational form and proving absoluteness. The sheer number of concepts is an obstacle, and some of them are hard to express in relational form, especially those involving recursion. Most of the relations have to be re-expressed using an internal datatype of formulae.
My formalization has two limitations. First, I am not able to prove that L satisfies the axiom scheme of comprehension. Although Isabelle/ZF handles schematic proofs easily, the proof of comprehension for the formula requires an instance of the reflection theorem for . Each instance of comprehension therefore has a different proof and must be proved separately. The reflection theorem is proved by induction (at the metalevel) on the structure of ; thus, all these proofs are instances of one algorithm, and they are generated by nearly identical proof scripts [18]. The inability to prove the comprehension scheme makes the absoluteness proofs harder: every necessary instance of comprehension is listed. Instantiating these proofs to L has required proving that each of those instances held in L. There are about 35 such instances.
My formalization has another limitation. The proof that L satisfies V = L cannot be combined with the proof that V = L implies the axiom of choice in order to conclude that L satisfies the axiom of choice. The reason is that the two instances of V = L are formalized differently: one is relativized and the other is not. Here I have followed the textbook proofs, which prove V = L, declare that the axiom of constructibility can be assumed, and proceed to derive the consequences of that axiom.
We could remedy both limitations by tackling the whole problem in a quite different way, by formalizing set theory as a proof system and working entirely in the metatheory. I leave this as a challenge for the theorem-proving community. A by-product of the work is a general theory of absoluteness for arbitrary class models of ZF. It could be used for other formal investigations of inner models. Future investigators might also try formalizing the proof that L satisfies the generalized continuum hypothesis and the combinatorial principle ♦.