Bedrock

Laying the groundwork for the metaphysics of V.

A machine-checked development, in Cubical Agda, of the set theory underlying contemporary questions about the universe of sets: forcing, inner models, and the structure of V. The immediate target is a full mechanization of L ⊨ GCH, with the cumulative hierarchy V realised as a higher inductive type. The full treatment is in the Charter.

This site is generated from literate Agda; this page is the book's reading catalog: the table of contents in learning order, which the chapter-end navigation also follows. For the structural view, by namespace, use the module tree in the sidebar. The mathematics proper is under construction: the groundwork, logic, and model parts are in place, and the parts on the cumulative hierarchy and the constructible universe follow.

{-# OPTIONS --cubical --safe --guardedness #-}
module Everything where

Landmarks: where the book ends up

  • Landmarks: the trophy case, displayed at the entrance: the milestone theorems restated as self-contained signatures with their full assumption bills, V⊨ZF (and its classical redemption), V⊨ZFC, and

L⊨ZFC, each hypothesis spelled in the name. Read it first to see the destination; understanding the signatures is what the rest of the book is for.

import Landmarks

Part 0: the groundwork

  • Base.Prelude: the curated host vocabulary (universes, paths, h-levels,

hProp, pairs, the indexing data), and the traceability discipline that governs how the book is read.

Impredicativity; interfaces only, nothing assumed.

lem→impredicativity).

  • Base.Choice: the boundary's second interface: set-level choice

SetChoice, stated levelwise like LEM, with Diaconescu's theorem mechanized at once: choice proves the excluded middle (choice→lem).

import Base.Prelude
import Base.Truth
import Base.Impredicativity
import Base.Classical
import Base.Choice

Part 1: first-order logic as an object of study

  • FOL.Syntax: the object language: a deeply embedded Formula with the constant domain as a parameter, intrinsic scoping, and every constructor primitive.
  • FOL.ZFStructure: the structures formulas talk about: carrier, equality, and membership, valued in a truth algebra; transitive classes and the restriction ↾.
  • FOL.Semantics: environments S ^ n, then evaluation ⟦_⟧ and satisfaction _⊨_ by structural recursion, each clause exactly its truth-algebra operation.
  • FOL.LevyHierarchy: the Levy hierarchy as inductive witnesses: the absence of unbounded quantifiers is Δ₀; above it, Σ₁/Π₁ and the alternating Σₙ/Πₙ tower.
  • FOL.Absoluteness: the Δ₀ absoluteness theorem abs₀ over a transitive class; Σ₁ transfers up, Π₁ down.
import FOL.Syntax
import FOL.ZFStructure
import FOL.Semantics
import FOL.LevyHierarchy
import FOL.Absoluteness

Part 2: what a model of ZF is

  • FOL.ZFModel: the axioms as a record: isZFModel with extensionality, meta-level regularity (the compactness ceiling), unique existence discharged by the description operator ℩, separation and replacement consuming the book's own formulas, and strong infinity through the numeral chain; isZFCModel adds choice as an extension.
import FOL.ZFModel

Part 3: the cumulative hierarchy realizes ZF(C)

  • V.Hierarchy: the library's higher inductive type V: sets as images of small families, extensional equality as a path constructor; the structure 𝒮ᵥ assembled directly, with extensionality and regularity banked free.
  • V.Smallness: the smallness toolkit: atoms compress through the library, connectives and bounded quantifiers pass smallness witnesses along,

separateFromSmall is the one pipe to sets; Δ₀-small makes Δ₀ separation an axiom-free theorem (separateΔ₀).

V⊨ZF from the excluded middle, and by Diaconescu V⊨ZFC from choice alone.

import V.Hierarchy
import V.Smallness
import V.Model

Part 4: the constructible universe

embed-⊨), Levy witnesses carried along (mapΔ₀ and the tower).

BoundedFo certifies, occurrence by occurrence, that a formula's constants satisfy a predicate, BoundedFo-mono weakens it, and

Relabel spends it: the certificate is the licence to relabel along a partial map, with meaning and Levy witness both carried across.

  • FOL.Manipulation.Parameters: constants out of the syntax and into the environment. They are counted (countFo) and collected (constantsFo) by occurrence, not by value, which is what makes a decidable equality on the constant domain unnecessary; placeFo puts each occurrence at the variable a placement names, in one pass and with no weakening lemma, and absFo instantiates it to the abstraction proper, raising the arity by the occurrence count and returning a parameter-free formula. ⊨-abs certifies that the trade costs no meaning, and

⊨-abs₁ with asPure₁ spend it at the arity a subset is carved by: a definable subset is carved by a parameter-free formula at a parameter vector, read in the inner semantics the definable powerset is defined by.

  • FOL.Coding: syntax as sets: ⌜_⌝ tags a constructor index onto the codes of the parts (constants coding themselves), and the inductive relation Codes is the interface, keeping code values out of the equations a typechecker has to normalize.
  • V.Coding: the hierarchy discharges both coding parameters: numerals are injective (#-inj) and Kuratowski pairs are injective (pr-inj), so formulas over V become sets of V.
  • L.Definability: the single step: Def A, the definable subsets of A with parameters from A: syntax as index set, inner satisfaction for meaning, essential smallness footing the bill; A ∈ Def A always, and A ⊆ Def A under transitivity.
  • L.Constructible: the tower Lset by membership recursion, one equation for zero, successors, and limits; the layer predicate

isLayer with layer-trans; the class isL and the structure 𝒮ʟ.

  • L.Ordinal: the supply of ordinals the closure arguments need: zero, successors and small unions are ordinals, and boundingOrd bounds any small family by a single ordinal. No comparison, hence no classical logic.
  • L.Rank: von Neumann rank by membership recursion, valued in the hierarchy itself: rank-ord makes it a measurement in ordinals and

rank-fix certifies it as the canonical index.

  • L.Ordinal.Linear: trichotomy ord-tri, and with it the L side's classical boundary: closure never had to decide anything, comparison does, so this chapter takes the excluded middle as a module parameter.
  • L.Ordinal.Stages: the ordinals of Lset α are exactly the members of α: rank-Lset and ord∈Lset→∈ say none appears early,

ord∈Lset-suc says none appears late.

  • L.WellOrder.Base: strict well-orders as a bundle (SWO), and the least element of a non-empty subset (leastOf), unique by trichotomy: the choosing device the axiom of choice takes. Reflection was expected to be a second consumer and is not, so there is exactly one, and it is

L.Choice.Transversal, the last chapter of the book.

  • L.Coding.Base: reading codes from inside: allCodes gathers every parameter-free formula's code into one nameable set, and

prAt / tagAt destructure a Kuratowski pair and a tag in bounded form, Δ₀ and adequate.

lookup-spec; memPairAt reads a value, sucAt

recognizes the index shift under a quantifier, and seqSet collects all finite sequences over a set.

  • L.Stage: the least ordinal satisfying any property of ordinals, by well-founded descent and unique by trichotomy; the earliest stage containing a constructible set is its first instance, sealed so the descent never reaches a later conversion problem.
  • L.Axioms.Basic: the first five model fields. Extensionality and regularity descend along transitivity; uniqueness then comes free; and the empty set, pairing and union are each carved out of one stage by one formula.

finSetL generalizes the pairing argument to any finite family drawn from a stage, which is how a recursion's table of values reaches L.

Lset-suc identifies the successor stage with the definable powerset of its predecessor, which is what puts that powerset in L as 𝒟ₒS. Pairing's carving is stated on its own as a fact about the tower:

pair∈Lset-suc puts the unordered pair of two members of a stage in the next stage, and pr∈Lset-suc the ordered pair two stages up, which is what places anything written with ordered pairs at a stage at all.

  • L.Axioms.Separation: separation and replacement for Δ₀ formulas, at a stage holding the argument and the formula's constants; the content is that membership in the carved set is satisfaction in the model.
  • L.Reflect: Montague's argument, answering a class-sized existential inside a set. A ladder is an ascending chain of ordinals; if each rung's environments have their answering stages on the next, its limit reflects the existential for every tuple of parameters it contains. Single is the ladder for one matrix. Taking the least stage rather than the least witness is what keeps the well-ordering of L out of it.
  • L.ReflectFo: the same for a whole formula, by structural induction. A jointly built ladder answers for every matrix of a formula at once, and

mkReflect then names a stage at which the formula agrees with its relativization to it, trading arbitrary complexity for Δ₀ and a stage.

  • L.Axioms.Numerals: the numeral chain inside L, pinned to the hierarchy's numerals by projection equations. Entirely constructive, which is why it is separate: the excluded middle enters infinity only at the collection step.
  • L.Axioms.Infinity: the numeral chain inside L, pinned to the hierarchy's numerals by projection equations for the model's own pairing, union and successor.
import FOL.Manipulation.Relabelling
import FOL.Manipulation.Bounding
import FOL.Manipulation.Parameters
import FOL.Coding
import V.Coding
import L.Definability
import L.Constructible
import L.Ordinal
import L.Rank
import L.Ordinal.Linear
import L.Ordinal.Stages
import L.WellOrder.Base
import L.Coding.Base
import L.Coding.Environment
import L.Stage
import L.Axioms.Basic
import L.Axioms.Separation
import L.Reflect
import L.ReflectFo
import L.Axioms.Full
import L.Axioms.Power
import L.Absoluteness
import L.Coding.Model
import L.Coding.InL
import L.Coding.Closed
import L.Recursion
import L.Coding.EnvSet
import L.Coding.Sat
import L.Coding.Bridge
import L.Coding.Table
import L.Coding.Sound
import L.Coding.Unique
import L.Coding.Slot
import L.Coding.Descent
import L.Coding.Shape
import L.Coding.Recover
import L.Coding.CodeSet
import L.Coding.Graph
import L.Coding.Satisfaction
import L.Coding.Uniform
import L.Coding.Powerset
import L.Coding.Sequence
import L.Hierarchy
import L.Axioms.Numerals
import L.Axioms.Infinity
import L.Choice.Stage
import L.Choice.Finite
import L.Choice.Name
import L.Choice.Step
import L.Choice.Internal
import L.Choice.Table
import L.Choice.Faithful
import L.Choice.Adequate
import L.Choice.Limit
import L.Choice.Before
import L.Choice.Order
import L.Choice.Transversal

The root, stated today and finished over the remaining parts:

  • L.Axioms.Full: separation and replacement for arbitrary formulas, by reflecting the formula and applying the bounded instrument to its relativization; the confinement atom is what keeps replacement's image from escaping the stage.
  • L.Absoluteness: the bridge between the two object languages. A Δ₀ formula about the hierarchy whose constants are constructible is carried into the language of L by liftFo, and transferFo says the two say the same thing; the coding chapters stay on the hierarchy side and are quoted from here.
  • L.Coding.Model: the object language over the model. What "function" means (prAtL, appAt, svAt, domAt), the pair on the value side, the tag readers, environments, and extAt, the frame every set-valued clause is written in, whose two readings are its two projections. Constant-free readers are quoted through the bridge; readers naming a numeral are written fresh, since unbounded is now free.
  • L.Coding.InL: every code is an element of L, by one induction over the constructors with nothing in it. That is what lets a code be named as a constant of the model's object language, and a family of codes be the domain of an internalized recursion. The set of all codes is deliberately not proved to be one, and is not needed here. Also closure, the finite set of a formula's subformula keys, closure-inv reading it back, and

byTag, which matches the twelve constructors against the eight demands a closedness predicate makes, once rather than twelve times eight.

  • L.Coding.Closed: the closure satisfies the object language's closedness predicate, and is the least set that does. Eight instances of four readers, then one induction; the hypothesis a recursion over the subcodes of a formula needs about its index set, and the reason its value is unique. The eight clauses never look at a formula, so they are proved once for any set that peels (Peel: a member is merely the key of a formula whose own closure sits inside), and closureClosed is closedOf at a closure with closure-inv as its peeling. Generality is free because

byTag was already written against an arbitrary target set.

  • L.Coding.EnvSet: the environments over a set of L at a fixed length form a set of L, which is what the clauses that take a complement take it in. A small index type, one stage, one separation, and no recursion.
  • L.Coding.Sat: for a formula of the meta-language and a carrier, the set of environments satisfying it, by recursion on the formula. Nothing internal: each step names the previous steps' sets as constants, so each is one separation off the ambient set, and the internal clauses become identities rather than definitions. Exports the twelve values and their membership equations, and nothing else.
  • L.Coding.Bridge: what that value is. At every environment over the carrier, membership in it is satisfaction in the world (B, ∈), which is the notion the definable powerset is defined by; without the statement an internal Def read off the recursion would provably agree with nothing. The right-hand side is the inner semantics, not the ambient reading of the relativization, because only the inner one guards a bounded quantifier twice, as the condition does. defSet-Sat spends it on L.Definability directly. The registered coherence risk does not fire: indexing the bridge by the inner environment vector makes a quantifier's extension consing on the underlying family, so the coherence is two refl branches shared by all four quantifier clauses, and the truncated recovery is confined to the corollary that a member is nothing but an environment.
  • L.Coding.Table: the entries, one per subformula, and the two things a recursion wants of them: every member is an entry, and a key determines its value. The second is where the code equation's injectivity is spent, and the arity is eliminated by path induction so the equation is used at the single arity where it holds. Everything is an element of the model by construction, since the codes are the model's own.
  • L.Coding.Sound: the table satisfies the clauses, one at a time. Each verification is four moves and three are already built; what is left is a set identity, and those are cheap because the meta-level recursion defined its value by the very condition the identity reads back.
  • L.Coding.Unique: a table satisfying the twelve clauses over a subcode-closed index records at each key the value the recursion built there, which is what makes the graph single-valued. Stated against the canonical value and with the index a variable, because a key substituted into a satisfaction does not typecheck in any reasonable time.
  • L.Coding.Slot: the slot a formula's recursion is indexed by satisfies the object language's closedness predicate, which is the hypothesis the satisfaction graph states about its index set. The closure chapter's theorem again, on the model's own coding.
  • L.Coding.Descent: how a recursion on codes gets from a code to its parts, which membership will not do: Kuratowski's pair puts a part four membership steps down and the sets in between are not codes. Rank increases strictly along membership, so the four steps compose by transitivity of ordinals and the recursion runs on the rank instead.
  • L.Coding.Shape: the half of "is a code" that closedness does not say. Closedness is eight implications keyed by tag, so a member with no recognized tag satisfies all eight vacuously; shapedAt says every member is an arity-tagged pair whose tag is one of the twelve, with the payload that tag calls for. Two frames carry the twelve, because twelve tags have two payload shapes between them; what else a tag demands is a relation the frame carries, and isTmAt is the one such demand that is not about a formula code. Shapedness is stated at two slots, the set and a carrier, because a term has two things to bound and they are different: a variable's index by the arity numeral, a constant by membership in the carrier. The second is what makes a member the key of a formula over that carrier rather than over the model, and it is written at a slot rather than as a constant so that nothing below is re-indexed. isTmAt-decode recovers the term over any alphabet, which is the first decode and the only one needing no induction; its constant clause needs one thing the predicate cannot supply, that the carrier's members are the alphabet's image, and takes it as a hypothesis.

Peel.peel is the two halves meeting: shapedness says which of the twelve a member is and hands back its parts, closedness says those parts are members too at the arity the tag calls for, and neither alone is a step of a recursion. The other direction is owed as well, since a predicate written to be consumed proves nothing until something satisfies it:

shaped-in builds the twelve-fold disjunction from one choice per member, and closureShaped spends it on the closure of a formula, which is the second hypothesis the decode's first caller owes. A measurement worth keeping: the two disjuncts of isTmAt are read by two named lemmas, and inlined as two clauses of one function the chapter does not finish in ten minutes, because a branch whose type is inferred is solved against the whole disjunction rather than against its own disjunct.

  • L.Coding.Recover: the decode. In a set that is closed and shaped at a carrier, a member handed over as a key at a stated arity is the key of a formula over that carrier, and Decode.recover produces it. The alphabet is a parameter and the target is stated over it, because the consumer indexes by the formulas over one carrier and a formula over the model would be useless to it. That also makes the six frames shorter: over the model each had to bridge the model's coding to the hierarchy's before comparing a code with a payload, and over the alphabet the code already is an element of the hierarchy. That every member is such a key is not proved here and is owed by whoever builds the set, since shapedness puts no condition on the arity component it binds. The recursion runs on the rank of the code, not on the code and not on the key: not on the code because membership does not descend into a Kuratowski pair, not on the key because rank arithmetic on a pair is a fact nobody has proved. The arity rides alongside as a natural number, which is what lets the induction come back at the larger one a quantifier raises it to; the carrier is not quantified over at all, being a slot fixed before the induction starts. Six frames carry the twelve cases, and each takes its constructor's coding equation as a hypothesis, because with the constructor a variable the coding function does not reduce and finding that equation is the whole cost. Over the alphabet those twelve equations are still refl, since relabelling commutes with every constructor definitionally.
  • L.Coding.CodeSet: the codes at a carrier, as sets of L, one at arity one and one at every arity. smallDom contains the keys in a stage and general-formula separation cuts them back, so the chapter is two object-language predicates that differ in one conjunct. The shared conjunct, "there merely is a carrier equal to A and a closed set shaped at it holding this", is unbounded existentials and free here; the carrier is a slot in hasWitnessAt and becomes a constant only one binder up, in hasWitness, which pins it with var zero ≐ con A. That split is forced by the consumer: the internal hierarchy binds its stage, and a set enters a formula only by being named, so a predicate that names its carrier cannot be spoken under that binder at all. The conjunct that differs says the member is a pair whose first component is a numeral, and it exists because recover takes its argument as a key at a stated arity while neither closedAt nor shapedAt constrains the arity slot: shapedness binds it existentially with no condition, so the set must pin it from outside. isCode names the numeral one; isCodeAny binds the arity and asks only that it lie in ωʟ, which reads back without an induction because ω-specL is an equation and the numeral chain projects. Codes-spec and AllCodes-spec close both round trips: a member is exactly a key of a formula over the carrier, at arity one and at some arity respectively, so both sets are characterized rather than caught between two statements. The all-arity set exists for the class it characterizes: a recursion over codes answers at a code's subcodes, a quantifier's subformula lives one arity up, and the arity-one class does not contain it, so it cannot be a domain.
  • L.Coding.Satisfaction: the instance. The slot is the domain, the graph is the previous chapter's, and the two halves meet in funct: existence hands the graph the objects already built, uniqueness pins any table the graph accepts against the one the meta-level recursion built.
  • L.Coding.Uniform: the same satisfaction over the codes at a stage, which is the domain every consumer wants: one formula's slot gives a table per formula, and a consumer arrives holding a code, not a formula it is a subcode of. AllCodes is the domain, and nothing else moves, because the graph binds its table existentially: funct need only exhibit some admissible table holding the member, and the smallest is the subformula slot of the member's own formula. So Table, Slot, Sound and Unique are applied at their existing types and the registered re-indexing at (carrier, key) never happens. The one new thing bridges the two codings, the hierarchy's over the stage's alphabet and the model's over the model's language: codeBridge, written for this and unused until now, plus functoriality of relabelling. val-at reads the value out at a member given as a key, val-sat says that value is satisfaction over the carrier, and val-defSet lands it on the definable powerset at arity one. The code carrier and the environment carrier stay independent parameters, and are pinned together only where satisfaction has a meaning. Every reading takes the member as a variable with its key equation beside it, and the name a consumer would write instead, keyIn, is sealed where it is built: written out, the key's construction lands inside a satisfaction and no length of proof elaborates.
  • L.Coding.Graph: what the satisfaction recursion's graph says. Three existentials over the index set, the table and the carrier, guarded by closedness, totality and the twelve clauses, with the value read off the table. Everything is bound because a graph may not name a table it has not been given, which is the one thing the internalization theorem forbids. One frame with two instances, because the pinning clause is the frame's parameter:

satGraphAt takes the carrier as a slot, for a consumer whose carrier is itself a bound variable, and satGraph pins it to a constant, at the type and the witness tuple it always had.

  • L.Coding.Powerset: the definable powerset described in the object language at a carrier that is a slot, and the step the whole route exists for. The internal hierarchy binds its stage, so a description that names its carrier cannot be spoken there at all; DefAt names nothing. It says that u is the set of exactly those x for which there merely are a code c over the carrier and a value v, with v what the satisfaction recursion records at c and x the set of members of the carrier whose one-entry environment lies in v. The two existentials are adjacent, which is a correction a probe forced: separated by a conjunct, the code hypothesis and the satisfaction hypothesis land at different environments and the route acquires a weakening lemma it otherwise never needs. DefinesAt is the third conjunct alone and envOneAt the one-entry environment, one line because a graph of length one is a single pair. DefAt-in says the operator satisfies the description and DefAt-out that nothing else does, the second under DefOK: every existential in the description ranges over L and can reach only what lives there, so the description is adequate exactly where the carrier's definable subsets are constructible. That side condition is a hypothesis of the elimination alone, since the introduction's own hypothesis implies it, and at a stage it is discharged for good by the successor identity, leaving DefAt-stage: an equation of truth values saying the description holds of 𝒟ₒS and of nothing else.
  • L.Coding.Sequence: the hierarchy said as a sequence, which is the only shape a graph for it may take. A graph may not name the object it defines and the tower at a stage is built from the tower below it, so what is written instead is what an approximation is. StepAt is the step at an argument: one extAt over three adjacent existentials, the argument, the value the approximation records there, and its definable powerset, the last bound rather than named because the previous chapter delivers a description of it and not a term for it. One extAt rather than a hand-made pair of inclusions, because a pair would duplicate the three existentials and hand every reading back in two halves that are not each other's inverse. One side condition PowOK serves both directions, since a definable powerset that is an element of L is one whose members are constructible.

ApproxAt is two conjuncts and no more: f is defined exactly on the argument's members, and every value it records is the step there computed from f itself. It is a membership equivalence rather than a one-directional collection, which keeps the coming induction's motive a proposition and removes an internal function-extensionality lemma from the route; and it carries no single-valuedness conjunct, because the step condition already pins every value recorded at an argument, so single-valuedness is a corollary rather than three universal quantifiers under a satisfaction. LsetGraph binds the approximation over the two. The chapter's entire price was conversion: its two graph readings stated at concrete slots cost 98 seconds of 130, and each place where a hypothesis wrote an environment out while the application named it behind an abbreviation cost 15 more. Written so that the two sides are the same expression it checks in under two seconds, which extends the variable-argument law from a substitution to a statement.

  • L.Hierarchy: the graph of the last chapter proved against the tower the book actually built, and the internal hierarchy it is proved with. A table is a set of ordered pairs; it is correct on a set when every value it records below that set is the meta tower there, and complete when it records one at every argument below. step-Lset reads a satisfied step off a correct table and gets the tower back, step-table writes the step from it, and the previous chapter's side condition is discharged inside both, since a recorded value is the tower at an ordinal and the definable powerset of a stage is constructible. approx-val is one membership induction on the argument whose motive quantifies over all recorded values, so single-valuedness is never a hypothesis and approx-uniq falls out in three lines. Lset-only and Lset-defines are the graph's two directions, and hierL is what the second is built from: the set of pairs of an ordinal with the tower's value at it, collected by replacement over a pair graph, with ordinality of each index taken from mem-ord untruncated and functionality filled through mereFunct. Its specification is a membership equivalence, which makes it unique and the induction's motive a proposition, and it is sealed where it is built. Two measurements, both about a name: the pair graph entering as a variable carrying its own equation, rather than as the closed sentence, is worth 85 seconds; and the set argument of mem-ord must be explicit at every use, since

IsOrd unfolds to a quantified membership and determines nothing. This chapter is what an internal definition of L is made of, and the internal well-order is read off it.

  • L.Axioms.Power: the power-set field, by bounding the constructible subsets and carving one stage. Condensation is not used and is not needed: the axiom asks that the constructible subsets form a set, not that they appear early.
  • L.Recursion: a function on a set of L whose graph is expressible has its table in L. A corollary of general-formula replacement, not a theorem: the usual absoluteness discipline exists to make a table readable inside a stage, and nothing here reads inside a stage. The recursion stays in the meta-language where it was written; smallDom supplies the domain for any small family, and Definition reduces an instance to a defining formula with its adequacy. witnessInModel records the one rule a graph must obey: an object-language existential ranges over L, so a graph may not describe an object by asserting that object's existence.
  • L.Choice.Stage: where a set of L first has a member, which is what replaces a well-ordering of L. μ is the earliest stage meeting it, one instance of the least-ordinal operator and sealed like stage;

meet-suc makes that stage a successor, because a set enters the tower only by being carved out of the stage below, and defStage is the stage it succeeds, a function because a successor determines what it succeeds among ordinals (ord-suc-inj). Lset-μ identifies the stage of first appearance with the definable powerset over the definition stage, so a first member carries a name written over one fixed stage, and that is what the choosing device compares. stageBound is the ordinal the bookkeeping runs in: above a set's own stage, hence above its members and theirs by transitivity, and above ω, where the names themselves live. No relation on L is stated here and no recursion is run.

  • L.Choice.Finite: the finite stages are finite, and each carries a well-order. Tally is the whole finiteness vocabulary, a finite family hitting every member, with neither injectivity nor decidable equality asked for; powerTally raises one to the definable powerset by enumerating the bit vectors over it, since every subset of a tallied stage is definable (finSet∈𝒟ₒ), and stageOrder runs that step along the numerals. precedes compares two subsets at the earliest point where they disagree: irreflexive for free, transitive by comparing two witnesses, trichotomous by the excluded middle with the base's smallest elements. Its well-foundedness is no property of the comparison at all, and would fail over an infinite base; it is bought from the tally through Search, where a scan of a finite family returns a smallest element of any inhabited property and the classical step turns that into accessibility. limitOrder assembles Lset ω with the level as the primary key, because the earliest-disagreement orders do not extend one another and with the level in front they do not have to; it is the first exercise of

L.WellOrder.Base, twice over, since the levels are ordered there too.

Name is an arity, a parameter-free formula of one more variable, and a vector of parameters from the stage below; denote is the subset it carves, read in the inner semantics Def is defined by (denote-mem) and in the internalized table (denote-table), and names-complete says every member of the successor stage has a name. code∈limit puts a parameter-free code in Lset ω, because it is built from numerals and pairs and nothing else, and

code-inj makes it faithful by erasing the constants back out.

_≺ₙ_ is the three-key lexicographic comparison written out, code then arity then parameters, with all four SWO laws and leastName, the least name of a non-empty family.

  • L.Choice.Step: one order at every stage, as a family. birth is the ordinal a constructible set is carved over, one below the earliest stage containing it, and it exists for the reason the choice-stage chapter gave for a cell: a set enters the tower only by being carved out. stepAt is the step, from a well-order of Lset δ to one of Lset (sucV δ), in one branch: the order is by least name everywhere, the previous chapter's three-key comparison pulled back along a map that is a function precisely because the stage below is well-ordered. A first draft guarded a second branch below the limit stage; measured, it was surplus, and what it really contributed was a normalization barrier that the opaque seal gives more cheaply. pullOrder moves a well-order along an injection and is the only transfer written: the step uses it, and so does

carry, the presentation of a stage's members as the index type the naming chapter takes. Three definitions and two readings say what the pulled-back order is for a caller outside: denotesAt, a set's names;

IsLeastName, the well-order chapter's IsLeast at that family and never a re-spelling of it (16 s against nothing, because a comparison at a computed name opens the code order); leastNameOf, the search; and stepAt-fill/stepAt-read, the step against the name order at any two names the caller has shown least, proved inside the telescope the seal lives in, since restating either at top level costs 39 s. No order on dependent sums is built. orderAt is the family itself, all four SWO laws at every ordinal, by membership induction, and it is sealed, since an unsealed order unfolds into a recursion over the hierarchy. Its comparison takes the birth as the primary key, which is why

endExtension then costs nothing: a comparison never mentions the stage it is read at, so the order at a large stage restricted to a small one is a path to the order there, not merely an equivalence, and the only work is the proof-irrelevance of constructibility and of ordinal-hood.

  • L.Choice.Internal: the same order, described in the object language, so that the model's own separation can carve it out. InLimitAt is the skeleton's stage condition, and it is one membership atom in the limit stage, said through LsetGraphAt at the constant ωʟ: a parameter-free code is hereditarily finite, so the recursion that would have decided constant-freeness from inside is never written. It is not constant-freeness, though, since a hereditarily finite code may name hereditarily finite constants; FreeAt is, and it is one membership atom too, in the code set at the empty alphabet, resting on the fact that a parameter-free formula has the same code at either alphabet (freeCode-in, freeCode-out). Read at slots (codeFree-out) the skeleton slot holds exactly the codes of the parameter-free formulas of one more variable than the arity, which is exactly a meta name's formula, and codeFree-limit derives the stage condition from it. NameAt is a name at slots, a skeleton in the limit stage and free of constants, a parameter sequence over the carrier whose domain is the arity, and a denotation written as one extAt whose condition reads the value satGraphAt assigns at the key the arity and the skeleton make; two code sets reach it as slots, the one at the carrier, without which the graph's existentially bound table pins nothing, and the one at the empty alphabet, without which the skeleton is not a meta name's. ≺At runs no recursion of its own: a membership atom against the order-so-far for the code, a membership atom between numerals for the arity, and a bounded lexicographic quantification for the parameters, with both orders reaching the description as slots.

StepAt is one step of the family, by least names, with one branch, so the min-difference formula the plan once wanted is not needed.

order-in and order-out are the two adequacy halves, at variable slots in a variable environment: with each relation slot carrying the hypothesis that says which order it holds, the formula holds of two names' data exactly when _≺ₙ_ holds of the names, the parameter key bridged by an induction identifying a first difference with the naming chapter's recursion on vectors.

  • L.Choice.Table: that order, turned from a description into an object, one at every ordinal. Related is the class realized, the pairs of two members of a stage the order there relates, carrying the comparison truncated because a strict well-order is not known to be proposition-valued, and strict takes the truncation off again for every such order at once by splitting on trichotomy before eliminating anything. ApproxAt and GraphAt are the approximation and its graph, shaped as in L.Coding.Sequence but generic in the step condition, which enters as a parameter in two forms with one meaning, at slots because the graph must bind the table it consults and at constants because separation carves with a formula of one free variable.

approx-val pins every value an approximation records by one membership induction on the argument, with no single-valuedness hypothesis anywhere, and approx-uniq is the corollary. tableAt is the construction, sealed where it is built, and it carries two things at every ordinal, unlike the hierarchy chapter's: the table of relations below it, collected by replacement through mereFunct, and the relation at it, separated out of a bound, because the order at a stage has no meta-language term to exhibit. That bound costs one appeal, since the pairs of two members of a stage are a small family of elements of L, so smallDom confines them all at once. rel-fill, rel-rep, ixRel-fill and

ixRel-rep read the membership of any set that realizes the class, at the two shapes a member of a stage comes in, the second of which is what a separation and the naming chapter's parameter order both consume; stating them of any realizing set is what puts them a stage earlier than the construction, where the naming machinery needs them, and relL-fill,

relL-rep, ix-fill and ix-rep are those four at the set this chapter builds. What is left open is the step condition's own adequacy, which is the previous chapter's StepAt against the meta step, named here as the two hypotheses of Described.

  • L.Choice.Faithful: the description made faithful, and the frame's two hypotheses discharged down to one. BirthAt is the birth stage said in the object language, and it names no constant and needs no successor operation: the tower at the slot does not hold the set while the definable powerset of that tower does, which Lset-suc makes equivalent to being one below the least stage containing it, spent only on the meta side. BirthAt-out and

BirthAt-in are its two readings at variable slots with ordinality the only hypothesis, soundness being a trichotomy against the least stage written as a named helper. isCodeAnyAt is the code predicate at any arity over a carrier held in a slot, and it is an instantiation and not a construction: the arity-bound conjunct and the witness conjunct both already existed, and only their meeting is new; CodesAt is the set they cut out, one extAt, whose two readings pin the slot to the code set over the carrier, so the naming description's code-set slot is pinned by description rather than by an outside equation. order-unfold is the order family's defining equation at a stage, one cong over the recursion's computation rule; bornIn is the converse of birth-in, and it buys the description one binder less;

stepMoved carries a step comparison along an equality of carriers, rebuilt locally rather than reached for in another module. CondCore is the order at a stage described in full, birth-primary, generic in the step condition: it binds four sets, takes the stage as a term so that the constant form costs no binder, and is sealed where it is built. Cond, Cond₀,

cond-spec and cond₀-spec are the two forms the previous chapter's frame asked for together with their meanings, so Described applies and everything it proves is available, conditional on the step parameter and on nothing else. Four measurements are recorded in the chapter because each is a law and not a preference: the two elements a birth description is satisfied at must be sealed (178 s against 2 s), an environment must be spelled out rather than abbreviated (207 s against 3 s), a two-way split concluding in a satisfaction must be a named helper and never a with (past 300 s), and a description read at constants must be sealed where it is built (160 s per reading). What is not here is the step's own adequacy, L.Choice.Internal's StepAt against

stepAt, which enters as the parameter Stp with stp-out

and stp-in as its meaning: the first takes the table's correctness at every value recorded at the carrier, since the condition it reads may bind a value of its own, and the second takes a single value that realizes the order there, since that is what it has to put in.

  • L.Choice.Limit: the order on the members of the limit stage, as an element of L, which is what the internalization frame's code slot has been asking for. LevelAt is the level said in the object language, three conjuncts and no constant but ω: the slot holds a member of ω, the tower there holds the set, and no smaller numeral's tower does. Both readings stand at variable slots, with the level arriving as a variable numeral carrying its own defining equation, which is the difference between 145 s and 1.8 s, since the level is a classical accessibility recursion and conversion at a slot forces it open. PrecedesAt is one step of the earliest-disagreement comparison with nothing concrete in it: the base relation and the base stage are held in slots, so the description can stand where the relation is the value of a recursion, and the base relation's membership is reached by appAt, since a pair is described and not named. strictLimit takes the truncation off a comparison by splitting on trichotomy first.

LimitOrdAt joins the two keys as a disjunction whose first disjunct binds two levels and compares them by membership and whose second binds one, so an equation between levels never enters the object language.

pairsBound confines every pair the order could relate by

smallDom, and codeOrder is the separation out of it, sealed where it is built; codeOrder-fill and codeOrder-rep are the two representation lemmas, and CodeKeys.AtParams is

Adequacy.Keys with its code slot filled by them, at the same two arguments and with no adapter. All of it is conditional on one hypothesis,

BeforeAt with its two readings against before, which is the earliest-disagreement family along the numerals said inside: a recursion whose values are relations, so an approximation, cheaper than the tower because the index is a member of ωʟ and the step is already written. Two measurements, each an old law in a new place: a case split whose scrutinee is a bundle's comparison and whose conclusion is a satisfaction does not finish, and written on an explicit sum with named branches it costs nothing (past 300 s against 2.4 s); and the composed description must be sealed where it is built, since the separation's condition unfolds it under two binders (past 300 s against 2.7 s).

  • L.Choice.Before: the earliest-disagreement family, internalized, which discharges the one hypothesis the previous chapter was left standing on.

relAt is the relation at each numeral as an element of L, a separation over the pairs of that finite stage carved with the previous chapter's step description, whose two slots are bound and pinned to constants by the object equality, so one description serves both the separation and the graph; relAt-out and relAt-in are its two readings, proved together by induction on the numeral, each spending the other at the predecessor because the previous relation is consulted only inside the agreement clause, and precedes-map carries that comparison contravariantly. RelBodyAt is the step, generic in the member, the index and the approximation, with the predecessor said as the ∈-maximal member of the index, so no object equality is needed and the step is empty at zero exactly where the recursion is. RelStepAt, ApproxAt and

RelGraphAt follow L.Coding.Sequence with no single-valuedness conjunct; step-rel and rel-step are the bridge to the meta-language, approx-val pins every value an approximation records by one well-founded induction with single-valuedness nowhere a hypothesis, and

rel-only is the graph's determinacy. approxSet is the approximation exhibited and costs no formula at all, since the approximation below a numeral is finite and finSetL spans it once

smallStage puts its members in one stage; beforeFam is the family, one replacement along ωʟ, sealed where it is built, with its two directions stated against the recursion and against no formula.

BeforeAt reads the family at the numeral held in a slot, with

appAtC for application at a constant and the two compared sets left unconfined, and with it Described is instantiated, so

codeOrder and CodeKeys are unconditional. One measurement, the largest in this part: the four descriptions must be sealed where they are built, since unsealed each satisfaction at a concrete environment normalizes a formula carrying two copies of the whole hierarchy description (376 s against 3.8 s, ninety-nine fold), and the frame that builds the family obeys the same law one level up by handing back a triple in which no formula appears.

  • L.Choice.Order: the step described, and the order table made unconditional. Stp is that description: a sealed formula binding six sets and pinning two constants. The six are the tower at the stage, reached through L.Coding.Sequence's LsetGraphAt; its definable subsets through L.Coding.Powerset's DefAt, with the two compared sets required to lie in it, which is how the step's two membership components arrive without a lemma nobody has; the table's value at the stage through

appAt, which is what keeps the description reading against whatever table the caller holds; and the code set over the tower through

L.Choice.Faithful's CodesAt, written for exactly this slot. The two pinned by an object equality are L.Choice.Limit's

codeOrder and the code set at the empty alphabet, because a slot holds a variable and those two are particular sets. The body at those seven slots is

L.Choice.Internal's StepAt. Slots supplies all six arguments of the step adequacy, generic in the six sets with their equations as hypotheses: the code side unconditional from the limit and family chapters, the carrier side from L.Choice.Table's readings at the bound value, which is the step parameter's own hypothesis and the only input taken from outside.

stp-out and stp-in are unpack and pack over the six binders, composed with L.Choice.Adequate's step readings and

L.Choice.Step's two, and they carry the frame's asymmetry: soundness quantifies over every value the table records there, completeness takes the single value the caller realizes with. One line then opens

L.Choice.Faithful.Ordered, and with it the whole of the table becomes unconditional: CondCore, Cond, Cond₀ and their two specifications, and, from L.Choice.Table, StepAt,

ApproxAt, GraphAt, approx-val, graph-only,

graph-table, tableAt, relL, relL-spec and all four representation lemmas. One measurement, a law at a new place: the type a frame concludes in is sealed where it is built, since instantiating that frame at the concrete elements the description binds normalizes it, and unsealed that does not finish (over 200 s against 7 s for the whole chapter).

Bound is the shape the last chapter separates with: the bounding ordinal of a set of L, the order on the members of the tower there as an element of the model, and its two representation lemmas.

  • L.Choice.Transversal: choice, and the frontier emptied. The axiom in the transversal form the model record states it: a set whose members are inhabited and pairwise disjoint has a set meeting each member in exactly one point. No well-order of L is used, because none exists here; a set is small, so L.Choice.Stage's bounding ordinal holds the family, its members and their members at once, and L.Choice.Order's Bound supplies the order on the tower there as an element of the model. Pick is the description, one free variable and two constants: some member of the family contains this set and nothing in that member precedes it, with the order pinned to a slot by an object equality because the atom for a pair in a relation reads the relation from a slot. pick-in and pick-out are its two readings against L.WellOrder.Base's IsLeast, every truncation payload named. transversalSet is the model's own separation by it over the tower, and transversal counts the intersection with each member: existence from leastOf, the least-element search that had waited without a consumer since it was written, and uniqueness from pairwise disjointness, which nothing else in the book uses, through

isPropLeastOf. The dependence on the supplied ZF model is one transport along the intersection's specification. hasChoiceL is the model's choice field, so the registry is empty and L.Frontier is deleted with the root chapter's second parameter. One measurement, and it is a law declining to bite: a description read at constants is sealed where it is built, worth ninety-nine fold where it was found and nothing here (2.3 s either way), since this description carries no coded syntax; the seal stays and the number is recorded, because the law is about what a description contains.

  • L.Model: the root chapter: the honest relative-consistency framing; extensionality and regularity descend along transitivity; L⊨ZF and

L⊨ZFC assembled, with the excluded middle as the only hypothesis. The debt registry L.Frontier that this chapter took as its second parameter is gone: it opened at eleven fields, shrank six times, and was deleted with the chapter that emptied it.

import L.Model

Tools in waiting

Chapters with, as of today, no consumer anywhere in the trunk; their first consumers arrive with Part 4's deeper machinery, and they read late so the main line stays unbroken.

  • FOL.Manipulation.Renaming: the book's entire variable calculus: renameFo on syntax, and the one correctness theorem ⊨-rename covering weakening, exchange, and contraction.
  • FOL.Manipulation.Relativize: tightening unbounded quantifiers to a constant bound, Δ₀ witness included, with the correctness equation.
import FOL.Manipulation.Renaming
import FOL.Manipulation.Relativize