# Bedrock > A machine-checked development of set theory in Cubical Agda. The constructible universe L is proved to model ZFC and to satisfy GCH. Bedrock is a machine-checked development, in Cubical Agda, of the set theory behind contemporary questions about the universe of sets. Two results are proved and both are stated in the chapter `Milestones`: `L⊨ZFC` and `L⊨GCH`, the constructible universe as a model of ZFC and as a model in which the generalized continuum hypothesis holds. Each rests on one hypothesis, excluded middle at `LEM (ℓ-suc ℓ)`, and on nothing else. The long-term aim is forcing, set-theoretic geology, the definability of ground models and the mantle. The project is host-language maximalist: every set-theoretic notion is rebuilt in type-theory-native idiom rather than transcribed from the textbook ZF axioms, and the deeply embedded first-order `Formula` is used only where syntax is itself the object of study. Every file typechecks under Agda 2.8.0 with the cubical 0.9 library and the `--safe` flag, so nothing here is postulated. This site is the development published as a trilingual mathematics textbook. One chapter is one Agda module. The displayed Agda is the formal content; the prose around it is the exposition, written in English, Chinese and Japanese from a single master. The reading order is a dependency order: a chapter's prerequisites are the modules it imports. ## How to read this site - Every chapter is at `//.html`, with `` one of `en`, `zh`, `ja`. The three editions share filenames, so swapping the language segment of any URL reaches the same chapter in another language. The one exception is the preview chapter `Milestones`, which has no page of its own: the reading guide embeds its whole body, so it is read at `//index.html#milestones`. The chapter list below gives every chapter's address, and `//reading-routes.json` gives it as data. - **Every chapter page has a plain-Markdown twin at the same path with a `.md` extension.** It carries the same prose and the same Agda in fenced blocks, with the chapter's stage, prerequisites and source in YAML front matter, and it is a fraction of the size of the HTML. Prefer it. Each HTML page advertises its own mirror with ``. - Pages are static HTML and need no JavaScript: the prose and the Agda are both in the initial response. - Anchors are stable and are the way to cite a passage. `#sec-0` is a chapter's title and `#sec-1`, `#sec-2`, ... its headings in document order. `#p-1`, `#p-2`, ... name its prose blocks, paragraphs and list items alike, in document order, so `#p-7` is the seventh block of prose on the page whatever section it falls in. Inside a displayed Agda block every token carries the character offset Agda's highlighter assigned it, as `#1234`, and every definition additionally carries its own Agda identifier as a named anchor, so `//V.Model.html#V⊨ZF` opens the page at that definition. - `//index.html` is the reading guide: routes, the dependency map, the milestone theorems and the glossary. ## Machine-readable endpoints Every one of these is static JSON, served with `Access-Control-Allow-Origin: *`. - [/en/reading-routes.json](https://bedrock.institute/en/reading-routes.json): the chapter graph: every chapter's localized title, learning stage, prerequisites, reading-order position, route memberships, and the `page` and `anchor` it is read at. This file decides those addresses; every link on the site is built from it. - [/en/terms.json](https://bedrock.institute/en/terms.json): the reader-facing glossary: each term's label in this language, a one-sentence recap, and the chapter that introduces it. - [/en/search.json](https://bedrock.institute/en/search.json): every Agda identifier Bedrock defines, with its module, its anchor on that module's page, its syntactic aspect and its type. - [/en/types/.json](https://bedrock.institute/en/types/.json): the elaborated type of every token of one chapter, keyed by the anchor that token carries in that chapter's URL. - [/sitemap.xml](https://bedrock.institute/sitemap.xml): every page, in every language, with hreflang alternates. - [/robots.txt](https://bedrock.institute/robots.txt): crawl policy. Nothing on this site is disallowed. ## Source - [https://github.com/BedrockInstitute/Bedrock](https://github.com/BedrockInstitute/Bedrock): the repository. A chapter is one literate Agda master at `src/.lagda.md`, and the site is generated from those masters by `scripts/site/render-site.py`. - [https://github.com/BedrockInstitute/Bedrock/blob/main/README.md](https://github.com/BedrockInstitute/Bedrock/blob/main/README.md): the project README, with the current measured size and build figures. - [https://github.com/BedrockInstitute/Bedrock/blob/main/docs/en/CHARTER.md](https://github.com/BedrockInstitute/Bedrock/blob/main/docs/en/CHARTER.md): the charter, the full methodological statement behind host-language maximalism. ## Chapters, in reading order Links point at the Markdown mirrors. Replace `/en/` with `/zh/` or `/ja/` for the Chinese or Japanese edition, and `.md` with `.html` for the page a human reads. A chapter that is not read at the page its own name gives says where it is read. - [1. Milestones](https://bedrock.institute/en/index.md) (`Milestones`, Preview), read at https://bedrock.institute/en/index.html#milestones: The book's proved endpoint results, with routes leading to each theorem. - [2. Prelude](https://bedrock.institute/en/Base.Prelude.md) (`Base.Prelude`, Foundations) - [3. Impredicativity](https://bedrock.institute/en/Base.Impredicativity.md) (`Base.Impredicativity`, Foundations) - [4. The classical boundary](https://bedrock.institute/en/Base.Classical.md) (`Base.Classical`, Foundations) - [5. Choice](https://bedrock.institute/en/Base.Choice.md) (`Base.Choice`, Foundations) - [6. The object language](https://bedrock.institute/en/FOL.Syntax.md) (`FOL.Syntax`, First-order logic) - [7. Structures](https://bedrock.institute/en/FOL.ZFStructure.md) (`FOL.ZFStructure`, First-order logic) - [8. Semantics](https://bedrock.institute/en/FOL.Semantics.md) (`FOL.Semantics`, First-order logic) - [9. The Lévy hierarchy](https://bedrock.institute/en/FOL.LevyHierarchy.md) (`FOL.LevyHierarchy`, First-order logic) - [10. Absoluteness](https://bedrock.institute/en/FOL.Absoluteness.md) (`FOL.Absoluteness`, First-order logic) - [11. Models of ZF and ZFC](https://bedrock.institute/en/FOL.ZFModel.md) (`FOL.ZFModel`, First-order logic) - [12. Mapping constants](https://bedrock.institute/en/FOL.Manipulation.ConstantMapping.md) (`FOL.Manipulation.ConstantMapping`, First-order logic) - [13. Variable renaming](https://bedrock.institute/en/FOL.Manipulation.Renaming.md) (`FOL.Manipulation.Renaming`, First-order logic) - [14. Constant relabelling](https://bedrock.institute/en/FOL.Manipulation.Relabelling.md) (`FOL.Manipulation.Relabelling`, First-order logic) - [15. Relativization](https://bedrock.institute/en/FOL.Manipulation.Relativization.md) (`FOL.Manipulation.Relativization`, First-order logic) - [16. Constant bounding](https://bedrock.institute/en/FOL.Manipulation.ConstantBounding.md) (`FOL.Manipulation.ConstantBounding`, First-order logic) - [17. Constants by occurrence](https://bedrock.institute/en/FOL.Manipulation.ConstantOccurrences.md) (`FOL.Manipulation.ConstantOccurrences`, First-order logic) - [18. Parameter abstraction](https://bedrock.institute/en/FOL.Manipulation.ParameterAbstraction.md) (`FOL.Manipulation.ParameterAbstraction`, First-order logic) - [19. Syntax as sets](https://bedrock.institute/en/FOL.Coding.md) (`FOL.Coding`, First-order logic) - [20. The cumulative hierarchy](https://bedrock.institute/en/V.Hierarchy.md) (`V.Hierarchy`, The ambient hierarchy) - [21. Small truth values in the cumulative hierarchy](https://bedrock.institute/en/V.Smallness.md) (`V.Smallness`, The ambient hierarchy) - [22. The cumulative hierarchy models ZF and ZFC](https://bedrock.institute/en/V.Model.md) (`V.Model`, The ambient hierarchy) - [23. Coding inside the cumulative hierarchy](https://bedrock.institute/en/V.Coding.md) (`V.Coding`, The ambient hierarchy) - [24. Definable subsets of a set](https://bedrock.institute/en/L.Definability.md) (`L.Definability`, Constructible stages and the axioms) - [25. The constructible hierarchy and universe](https://bedrock.institute/en/L.Constructible.md) (`L.Constructible`, Constructible stages and the axioms) - [26. Ordinal closure and finite ordinals](https://bedrock.institute/en/L.Ordinal.md) (`L.Ordinal`, Constructible stages and the axioms) - [27. Von Neumann rank](https://bedrock.institute/en/L.Rank.md) (`L.Rank`, Constructible stages and the axioms) - [28. Ordinals are linearly ordered by membership](https://bedrock.institute/en/L.Ordinal.Linear.md) (`L.Ordinal.Linear`, Constructible stages and the axioms) - [29. Locating ordinals in the constructible hierarchy](https://bedrock.institute/en/L.Ordinal.Stages.md) (`L.Ordinal.Stages`, Constructible stages and the axioms) - [30. The index of the least constructible stage](https://bedrock.institute/en/L.Stage.md) (`L.Stage`, Constructible stages and the axioms) - [31. The basic axioms](https://bedrock.institute/en/L.Axioms.Basic.md) (`L.Axioms.Basic`, Constructible stages and the axioms) - [32. Separation and replacement, bounded](https://bedrock.institute/en/L.Axioms.Separation.md) (`L.Axioms.Separation`, Constructible stages and the axioms) - [33. Existential reflection into a constructible stage](https://bedrock.institute/en/L.ExistentialReflection.md) (`L.ExistentialReflection`, Constructible stages and the axioms) - [34. Reflection for an arbitrary formula](https://bedrock.institute/en/L.FormulaReflection.md) (`L.FormulaReflection`, Constructible stages and the axioms) - [35. Separation and replacement, in full](https://bedrock.institute/en/L.Axioms.Full.md) (`L.Axioms.Full`, Constructible stages and the axioms) - [36. The power set in L](https://bedrock.institute/en/L.Axioms.Power.md) (`L.Axioms.Power`, Constructible stages and the axioms) - [37. From ambient formulas to formulas over L](https://bedrock.institute/en/L.Absoluteness.md) (`L.Absoluteness`, Constructible stages and the axioms) - [38. The numeral chain](https://bedrock.institute/en/L.Axioms.Numerals.md) (`L.Axioms.Numerals`, Constructible stages and the axioms) - [39. The axiom of infinity in L](https://bedrock.institute/en/L.Axioms.Infinity.md) (`L.Axioms.Infinity`, Constructible stages and the axioms) - [40. Formulas for singletons and pairs](https://bedrock.institute/en/L.Coding.PairFormulas.md) (`L.Coding.PairFormulas`, Internal coding: expressions and domains) - [41. Finite environments as set-coded graphs](https://bedrock.institute/en/L.Coding.Environment.md) (`L.Coding.Environment`, Internal coding: expressions and domains) - [42. Coding formulas over the constructible model](https://bedrock.institute/en/L.Coding.Model.md) (`L.Coding.Model`, Internal coding: expressions and domains) - [43. Formula expressions for coded recursion](https://bedrock.institute/en/L.Coding.Expressions.md) (`L.Coding.Expressions`, Internal coding: expressions and domains) - [44. Subcode-closed domains](https://bedrock.institute/en/L.Coding.Closure.md) (`L.Coding.Closure`, Internal coding: expressions and domains) - [45. Rank descent through coded pairs](https://bedrock.institute/en/L.Coding.Descent.md) (`L.Coding.Descent`, Internal coding: expressions and domains) - [46. Constructible codes and subformula trees](https://bedrock.institute/en/L.Coding.CodeConstructibility.md) (`L.Coding.CodeConstructibility`, Internal coding: expressions and domains) - [47. Closure under subformulas](https://bedrock.institute/en/L.Coding.SubformulaClosure.md) (`L.Coding.SubformulaClosure`, Internal coding: expressions and domains) - [48. The set of fixed-length environments](https://bedrock.institute/en/L.Coding.EnvironmentSet.md) (`L.Coding.EnvironmentSet`, Internal coding: tables and uniform satisfaction) - [49. Satisfaction by recursion on formulas](https://bedrock.institute/en/L.Coding.Satisfaction.md) (`L.Coding.Satisfaction`, Internal coding: tables and uniform satisfaction) - [50. Satisfaction and the recursion value](https://bedrock.institute/en/L.Coding.SatisfactionBridge.md) (`L.Coding.SatisfactionBridge`, Internal coding: tables and uniform satisfaction) - [51. Satisfaction tables over subformulas](https://bedrock.institute/en/L.Coding.SatisfactionTable.md) (`L.Coding.SatisfactionTable`, Internal coding: tables and uniform satisfaction) - [52. Agreement of environment sets](https://bedrock.institute/en/L.Coding.EnvironmentAgreement.md) (`L.Coding.EnvironmentAgreement`, Internal coding: tables and uniform satisfaction) - [53. Closing a code slot under its seven constructors](https://bedrock.institute/en/L.Coding.SlotClosure.md) (`L.Coding.SlotClosure`, Internal coding: tables and uniform satisfaction) - [54. Recognizing well-formed constructor keys](https://bedrock.institute/en/L.Coding.CodeShape.md) (`L.Coding.CodeShape`, Internal coding: tables and uniform satisfaction) - [55. Recovering formulas from codes](https://bedrock.institute/en/L.Coding.FormulaRecovery.md) (`L.Coding.FormulaRecovery`, Internal coding: tables and uniform satisfaction) - [56. Numerals in a successor-closed ordinal stage](https://bedrock.institute/en/L.Coding.NumeralBound.md) (`L.Coding.NumeralBound`, Internal coding: tables and uniform satisfaction) - [57. Quantifying over coded pairs and finite formula families](https://bedrock.institute/en/L.Coding.Quantification.md) (`L.Coding.Quantification`, Internal coding: tables and uniform satisfaction) - [58. Internalizing recursive definitions in L](https://bedrock.institute/en/L.Recursion.md) (`L.Recursion`, Internal coding: tables and uniform satisfaction) - [59. Graphs of recursive definitions](https://bedrock.institute/en/L.Recursion.Graph.md) (`L.Recursion.Graph`, Internal coding: tables and uniform satisfaction) - [60. The environment tower](https://bedrock.institute/en/L.Coding.EnvironmentTower.md) (`L.Coding.EnvironmentTower`, Internal coding: tables and uniform satisfaction) - [61. The set of all formula codes](https://bedrock.institute/en/L.Coding.CodeSet.md) (`L.Coding.CodeSet`, Internal coding: tables and uniform satisfaction) - [62. Describing the closed domain of formula codes](https://bedrock.institute/en/L.Coding.CodeDomain.md) (`L.Coding.CodeDomain`, Internal coding: tables and uniform satisfaction) - [63. Describing the satisfaction table](https://bedrock.institute/en/L.Coding.SatisfactionClauses.md) (`L.Coding.SatisfactionClauses`, Internal coding: tables and uniform satisfaction) - [64. The alphabet of formula codes](https://bedrock.institute/en/L.Coding.CodeAlphabet.md) (`L.Coding.CodeAlphabet`, Internal coding: tables and uniform satisfaction) - [65. Reading and validating the satisfaction clauses](https://bedrock.institute/en/L.Coding.SatisfactionClauseSemantics.md) (`L.Coding.SatisfactionClauseSemantics`, Internal coding: tables and uniform satisfaction) - [66. Pinning recursion on a subcode-closed domain](https://bedrock.institute/en/L.Coding.PinnedRecursion.md) (`L.Coding.PinnedRecursion`, Internal coding: tables and uniform satisfaction): Recursion pinned to a subcode-closed index set - [67. The satisfaction graph formula](https://bedrock.institute/en/L.Coding.SatisfactionGraph.md) (`L.Coding.SatisfactionGraph`, Internal coding: tables and uniform satisfaction) - [68. Uniform satisfaction over all codes](https://bedrock.institute/en/L.Coding.UniformSatisfaction.md) (`L.Coding.UniformSatisfaction`, Internal coding: tables and uniform satisfaction) - [69. A formula for the definable power set](https://bedrock.institute/en/L.Coding.DefinablePowerSet.md) (`L.Coding.DefinablePowerSet`, Internal coding: tables and uniform satisfaction) - [70. A sequence for the constructible hierarchy](https://bedrock.institute/en/L.Coding.HierarchySequence.md) (`L.Coding.HierarchySequence`, Internal coding: tables and uniform satisfaction) - [71. The constructible hierarchy inside L](https://bedrock.institute/en/L.Hierarchy.md) (`L.Hierarchy`, Internal coding: tables and uniform satisfaction) - [72. The first stage meeting a set](https://bedrock.institute/en/L.Choice.FirstIntersectionStage.md) (`L.Choice.FirstIntersectionStage`, The canonical well-order and Choice) - [73. Strict well-orders and least-element search](https://bedrock.institute/en/L.WellOrder.Base.md) (`L.WellOrder.Base`, The canonical well-order and Choice) - [74. Well-orders on finite stages](https://bedrock.institute/en/L.Choice.FiniteStageOrders.md) (`L.Choice.FiniteStageOrders`, The canonical well-order and Choice) - [75. Canonical names for successor-stage members](https://bedrock.institute/en/L.Choice.CanonicalNames.md) (`L.Choice.CanonicalNames`, The canonical well-order and Choice) - [76. Well-orders on all stages](https://bedrock.institute/en/L.Choice.StageOrders.md) (`L.Choice.StageOrders`, The canonical well-order and Choice) - [77. Formulas for name comparison](https://bedrock.institute/en/L.Choice.NameComparison.md) (`L.Choice.NameComparison`, The canonical well-order and Choice) - [78. An internal table of stage orders](https://bedrock.institute/en/L.Choice.OrderTable.md) (`L.Choice.OrderTable`, The canonical well-order and Choice) - [79. Adequacy of the stage-order description](https://bedrock.institute/en/L.Choice.StageOrderAdequacy.md) (`L.Choice.StageOrderAdequacy`, The canonical well-order and Choice) - [80. Adequacy of name comparison](https://bedrock.institute/en/L.Choice.NameComparisonAdequacy.md) (`L.Choice.NameComparisonAdequacy`, The canonical well-order and Choice) - [81. The limit-stage order inside L](https://bedrock.institute/en/L.Choice.LimitStageOrder.md) (`L.Choice.LimitStageOrder`, The canonical well-order and Choice) - [82. An internal family of earliest-disagreement relations](https://bedrock.institute/en/L.Choice.EarliestDisagreement.md) (`L.Choice.EarliestDisagreement`, The canonical well-order and Choice) - [83. The internal stage-order relation](https://bedrock.institute/en/L.Choice.InternalWellOrder.md) (`L.Choice.InternalWellOrder`, The canonical well-order and Choice): The internal canonical well-order - [84. Choice by a transversal](https://bedrock.institute/en/L.Choice.Transversal.md) (`L.Choice.Transversal`, The canonical well-order and Choice) - [85. The constructible universe models ZFC](https://bedrock.institute/en/L.Model.md) (`L.Model`, The canonical well-order and Choice) - [86. Small presentations of sets](https://bedrock.institute/en/V.Presentation.md) (`V.Presentation`, Ordinals, injections and cardinals) - [87. Ordinal indices, the Gödel pair order, and finite indices](https://bedrock.institute/en/L.Ordinal.SquareLaw.md) (`L.Ordinal.SquareLaw`, Ordinals, injections and cardinals) - [88. Coded injections](https://bedrock.institute/en/L.Coding.Injection.md) (`L.Coding.Injection`, Ordinals, injections and cardinals) - [89. Cardinals and coded injections inside L](https://bedrock.institute/en/L.Cardinal.md) (`L.Cardinal`, Ordinals, injections and cardinals) - [90. Turning a definable injection into an internal code](https://bedrock.institute/en/L.DefinableInjection.md) (`L.DefinableInjection`, Ordinals, injections and cardinals) - [91. Composition and inclusion of coded injections](https://bedrock.institute/en/L.InjectionComposition.md) (`L.InjectionComposition`, Ordinals, injections and cardinals) - [92. The generalized continuum hypothesis inside L](https://bedrock.institute/en/L.GCH.md) (`L.GCH`, Ordinals, injections and cardinals) - [93. Cantor–Schröder–Bernstein for small presentations](https://bedrock.institute/en/V.CantorBernstein.md) (`V.CantorBernstein`, Ordinals, injections and cardinals) - [94. Cantor–Schröder–Bernstein inside L](https://bedrock.institute/en/L.CantorBernstein.md) (`L.CantorBernstein`, Ordinals, injections and cardinals) - [95. Collapsing a transitive well-founded relation](https://bedrock.institute/en/L.Mostowski.md) (`L.Mostowski`, Ordinals, injections and cardinals) - [96. An ordinal L-cardinal above every L-cardinal](https://bedrock.institute/en/L.CardinalAbove.md) (`L.CardinalAbove`, Ordinals, injections and cardinals) - [97. Assembling GCH from four internal bounds](https://bedrock.institute/en/L.GCH.Assembly.md) (`L.GCH.Assembly`, Proving GCH) - [98. An internal graph of uniform satisfaction](https://bedrock.institute/en/L.Coding.SatisfactionGraphSet.md) (`L.Coding.SatisfactionGraphSet`, Proving GCH) - [99. Soundness and completeness of the closed code domain](https://bedrock.institute/en/L.Coding.CodeDomainAdequacy.md) (`L.Coding.CodeDomainAdequacy`, Proving GCH) - [100. A Δ₀ description of the satisfaction table](https://bedrock.institute/en/L.GCH.SatisfactionDescription.md) (`L.GCH.SatisfactionDescription`, Proving GCH) - [101. A Δ₀ description of the definable power set](https://bedrock.institute/en/L.GCH.DefinablePowerSetDescription.md) (`L.GCH.DefinablePowerSetDescription`, Proving GCH) - [102. Adequate stages for the GCH argument](https://bedrock.institute/en/L.GCH.AdequateStages.md) (`L.GCH.AdequateStages`, Proving GCH) - [103. ω-recursion inside the constructible universe](https://bedrock.institute/en/L.GCH.OmegaRecursion.md) (`L.GCH.OmegaRecursion`, Proving GCH): Iterating a definable step through ω - [104. The Mostowski collapse](https://bedrock.institute/en/V.Collapse.md) (`V.Collapse`, Proving GCH) - [105. Building and collapsing a Skolem hull](https://bedrock.institute/en/L.GCH.SkolemHull.md) (`L.GCH.SkolemHull`, Proving GCH) - [106. A Δ₀ description of the constructible hierarchy](https://bedrock.institute/en/L.GCH.HierarchyDescription.md) (`L.GCH.HierarchyDescription`, Proving GCH) - [107. Transferring structure through condensation](https://bedrock.institute/en/L.GCH.CondensationTransfer.md) (`L.GCH.CondensationTransfer`, Proving GCH) - [108. Ordinals below a successor cardinal inject into its base](https://bedrock.institute/en/L.GCH.BelowSuccessorCardinal.md) (`L.GCH.BelowSuccessorCardinal`, Proving GCH) - [109. Constructing order types inside L](https://bedrock.institute/en/L.GCH.OrderType.md) (`L.GCH.OrderType`, Proving GCH) - [110. Choosing a cardinal representative for an ordinal](https://bedrock.institute/en/L.GCH.CardinalRepresentative.md) (`L.GCH.CardinalRepresentative`, Proving GCH) - [111. The square law for infinite L-cardinals](https://bedrock.institute/en/L.GCH.CardinalSquareLaw.md) (`L.GCH.CardinalSquareLaw`, Proving GCH) - [112. The least-witness map inside a constructible stage](https://bedrock.institute/en/L.GCH.LeastWitnessMap.md) (`L.GCH.LeastWitnessMap`, Proving GCH): Least witnesses form a definable map - [113. Injecting the successor cardinal into the power set](https://bedrock.institute/en/L.GCH.SuccessorIntoPowerSet.md) (`L.GCH.SuccessorIntoPowerSet`, Proving GCH) - [114. Coding finite sequences below an infinite ordinal](https://bedrock.institute/en/L.GCH.FiniteSequenceCoding.md) (`L.GCH.FiniteSequenceCoding`, Proving GCH) - [115. The counting tools for infinite constructible stages](https://bedrock.institute/en/L.GCH.StageCountingTools.md) (`L.GCH.StageCountingTools`, Proving GCH) - [116. Locating the hull and its collapse inside L](https://bedrock.institute/en/L.GCH.ConstructibleHull.md) (`L.GCH.ConstructibleHull`, Proving GCH) - [117. Counting a Skolem hull from a counted start](https://bedrock.institute/en/L.GCH.HullCounting.md) (`L.GCH.HullCounting`, Proving GCH) - [118. Injecting an infinite constructible stage into its index](https://bedrock.institute/en/L.GCH.StageInjection.md) (`L.GCH.StageInjection`, Proving GCH) - [119. Bounded subsets appear at controlled stages](https://bedrock.institute/en/L.GCH.BoundedSubset.md) (`L.GCH.BoundedSubset`, Proving GCH) - [120. The constructible universe satisfies GCH](https://bedrock.institute/en/L.GCH.Theorem.md) (`L.GCH.Theorem`, Proving GCH) ## Other editions - [中文](https://bedrock.institute/zh/index.html): the same book. Chapter mirrors are at `/zh/.md`. - [日本語](https://bedrock.institute/ja/index.html): the same book. Chapter mirrors are at `/ja/.md`.