横断集合による選択

This chapter proves the axiom of choice at 𝒮ʟ in the transversal form used by the model record: given a set whose members are inhabited and pairwise disjoint, merely a set meeting each member in exactly one point.

The argument follows the classical proof, with its most laborious step already carried out earlier. The textbook well-orders the universe and takes the least member of every cell. A well-order of all of L is a relation on a proper class, and this book never built one; what the previous chapters built instead is a well-order of each stage, uniformly, and, at every ordinal, as an element of the model. That is enough, because a set is small. One ordinal bounds a family, its members and their members all at once, and inside the tower at that ordinal the choosing is an ordinary least-element search.

So the chapter is four moves. The bound: the stage chapter's bounding ordinal for the family, above the family's own stage and hence above every member of every member of it. The order there: the table's relation at that ordinal, an element of the model, with two lemmas reading membership in it against the meta comparison in both directions. The description: "some member of the family contains this set, and nothing in that member precedes it", a formula with the order as a constant, which the model's own separation cuts a set out with. The count: that set meets each member in exactly one point, existence from the least element and uniqueness from pairwise disjointness, which is what disjointness is for and the only place the book uses it.

There is a fifth thing, and it is an observation rather than a move. Choice is stated relative to a ZF model on this carrier, because the intersection it names is that model's derived operation; and the whole of that dependence is one transport along the intersection's specification.

One formula, one free variable, two constants. Of a set z it says: some member of the family contains z, and nothing in that member precedes z under the order. The application atom takes the order directly as a constant. The family is likewise named directly, since it appears only under a membership atom.

The formula is sealed, by the standing law that a description read at constants is sealed where it is built. Here that law is free rather than decisive: sealed and unsealed both check in 2.3 s, and the chapter says so rather than borrowing someone else's number. The reason is worth one line, because it says what the earlier measurements were really about. Those descriptions carried coded syntax inside them, and each satisfaction at a concrete environment normalized a whole hierarchy description; this one carries four atoms and one application, so there is nothing large to unfold. The seal stays, because it costs nothing and because a later reader of this description should not have to re-measure.

Perf: sealed by the standing law (a description read at constants), though measured here at 2.3 s either way: this description names no coded syntax.

The module fixes the ZF model supplying the intersection, the family, and the family's two hypotheses. The choice-stage construction supplies the bound and order at the family itself: β is an ordinal above the family's own stage, hence above its members and their members, and above ω where the names live; W is the well-order of the members of the tower at β; and rel is that same order as an element of the model, which is what lets it be named by a constant in the description at all.

Cell x is the predicate "is a member of x" on those members, and least applies the generic search from L.WellOrder.Base to it. The same search serves finite-stage orders and name selection, and will serve later GCH constructions; here its role is specific: it turns the stage order into one chosen representative for each cell. This is precisely the selection that excluded middle makes possible for the transversal.

pick-in and pick-out are the description's two readings, and neither is a corollary of the other: one builds a satisfaction out of a least element, the other extracts a least element from a satisfaction, and each has to move a set between the two ways it can be presented, as an element of L and as a member of the tower at β. Every truncation payload is named, Two and Predecessor, so that neither reading writes the nesting out; the negation is the one place a truncation is eliminated into the empty type, and it is eliminated in a named helper.

Then the separation and the counting. transversalSet is the model's own separation, at the tower at β, by the description. Cut fixes a member of the family: the centre of the intersection is the least element, which is in the transversal because pick-in says so and in the member because being least includes being there. Uniqueness is where pairwise disjointness is used. Another point of the intersection satisfies the description, so it is least in some member of the family; it also lies in this one; so the two members meet and are equal; so it is least in this member too, and least elements are unique by trichotomy alone. The generic uniqueness theorem isPropLeastOf closes precisely this last comparison.

ChoiceStatement is the statement the frontier used to hold, moved here verbatim and proved here: the model's choice field at 𝒮ʟ, relative to a ZF model on this carrier because the intersection is that model's derived operation. hasChoiceL gives the proof. The root chapter applies it to the very model it is assembling, which is why the statement quantifies over the model in the first place.

This line gives the Choice field used by the root theorem. Its statement remains relative to the ZF model being assembled because intersection is the derived operation of that model.

Pick is the description: some member of the family contains this set, and nothing in that member precedes it. pick-in and pick-out are its two readings against being a least element of a member. transversalSet is what the model's separation cuts out with it, over the tower at the family's bounding ordinal, and transversal counts the intersection with each member: one point, existence from the least-element search and uniqueness from pairwise disjointness. hasChoiceL is the model's choice field, and with it the frontier is empty and gone.

One measurement, and it is a law declining to bite. A description read at constants is sealed where it is built, and that law was worth ninety-nine fold where it was found; here it is worth nothing, 2.3 s either way, because this description carries no coded syntax. The seal stays, and the number is recorded so that the law keeps its true shape: it is about what a description contains, not about where it is read.

This is the end of the chain, so it is worth stating plainly what has been established. In cubical Agda, granted one instance of the excluded middle at the model's own truth level, the constructible universe is a model of ZFC. Read with the ambient-hierarchy result that the hierarchy models ZF, that is Gödel's relative consistency of choice in semantic form: a universe satisfying ZF contains inside it a sub-universe satisfying ZFC, so an inconsistency of ZFC would already be an inconsistency of ZF.

The costs are stated explicitly. The host is cubical Agda with its universe tower, informally about as strong as ZFC plus an inaccessible; excluded middle is a module parameter rather than an axiom, and it is the only hypothesis the theorem carries; and the development has no postulates or holes. This chapter supplies the Choice field that L.Model combines with the earlier ZF structure.