Bedrock

为 V 的形而上学奠基。

一项在 Cubical Agda 中的机器验证工作，针对当代集合宇宙问题背后的那部分集合论：力迫、内模型，以及 V 的结构。当前目标是完整机械化 L ⊨ GCH，其中累积层级 V 以高阶归纳类型实现。完整论述见纲领。

本站点由文学化 Agda 生成；本页是全书的阅读目录：按学习顺序排列，每章页尾的导航循此顺序。按知识结构浏览，请用侧边栏按命名空间分组的模块树。数学本体正在施工中：奠基、逻辑与模型诸部已就位，累积层级与可构造宇宙两部随后。

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

地标：本书的终点

Landmarks：奖杯陈列室，摆在入口处：里程碑定理以自足签名重述，假设账单全额陈列：V⊨ZF (及其精确价格版 V⊨ZF-impredicative)、单凭选择的 V⊨ZFC，与 L⊨ZFC。先读它，看清目的地；至于读懂这些签名，正是全书其余部分的任务。

import Landmarks

第零部：奠基

Base.Prelude：精选的宿主词汇 (宇宙、路径、h-层级、hProp、依值对与索引数据)，以及决定本书读法的可溯源纪律。
Base.Truth：真值代数 TruthAlgebra，零定律的运算签名，全书逻辑符号的唯一来源；附典范实例 hPropAlgebra。
Base.Impredicativity：尺寸词汇：isSmall；降层即「任意命题皆小」(Resizing)；小分类器 HPropSmallness；及其打包 Impredicativity。只有接口，无所假设。
Base.Classical：经典边界：排中律作为参数接口 LEM，与从它赎回的非直谓性诸接口 (lem→resizing、lem→hPropSmallness、lem→impredicativity)。
Base.Choice：边界的第二个接口：集合层选择 SetChoice，与 LEM 同款逐层级陈述；Diaconescu 定理当场机器化：选择证明排中律 (choice→lem)。

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

第一部：作为研究对象的一阶逻辑

FOL.Syntax：对象语言：深嵌入的 Formula，常量域作参数，作用域内蕴，构造子全原语。
FOL.ZFStructure：公式所谈论的结构：载体、等词与成员，取值于真值代数；传递类与限制 ↾。
FOL.Semantics：环境 S ^ n，与结构递归给出的求值 ⟦_⟧ 与满足 _⊨_，每条子句恰是对应的真值代数运算。
FOL.LevyHierarchy：作为归纳见证的 Lévy 层级：无界量词的缺席即 Δ₀，其上是 Σ₁/Π₁ 与交替的 Σₙ/Πₙ 之塔。
FOL.Absoluteness：传递类上的 Δ₀ 绝对性定理 abs₀；Σ₁ 向上、Π₁ 向下。

import FOL.Syntax
import FOL.ZFStructure
import FOL.Semantics
import FOL.LevyHierarchy
import FOL.Absoluteness

第二部：何谓 ZF 模型

FOL.ZFModel：公理作为 record：isZFModel 含外延公理、元层面的正则公理 (紧致性天花板)、经摹状词算子 ℩ 兑现的唯一存在、消费本书自家公式的分离与替换，以及经数码链的强无穷；isZFCModel 以扩展形式添加选择公理。

import FOL.ZFModel

第三部：累积层级实现 ZF(C)

V.Hierarchy：库的高阶归纳类型 V：集合是小族的像，外延相等是路径构造子；结构 𝒮ᵥ 径直装配，外延与正则免费入账。
V.Smallness：小性工具链：原子经库压缩，联结词与有界量词传递小性见证，separateFromSmall 是通往集合的唯一水管；Δ₀-small 让 Δ₀ 分离成为零公理定理 (separateΔ₀)。
V.Model：本部之巅：库存换形，替换与强无穷白得，第零部的 Impredicativity 为全分离与幂集标价；V⊨ZF-impredicative 以此精确价格合龙，主打的 V⊨ZF 由排中律赎回，经 Diaconescu 的 V⊨ZFC 则单凭选择。

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

第四部：可构造宇宙

FOL.Manipulation.Relabelling：常量变换，一次三个海拔：函子式 mapFo，无参公式的入口 embed，含义纹丝不动 (⊨-map、embed-⊨)，Lévy 见证随行 (mapΔ₀ 及其塔)。
FOL.Manipulation.Bounding：映射只是部分函数时的重标：BoundedFo 逐次出现地证明公式的常元满足某谓词，BoundedFo-mono 放宽它，而 Relabel 花掉它：证书就是沿部分映射重标的许可，含义与 Lévy 见证一并带过。
FOL.Manipulation.Parameters：把常量请出语法、请进环境。它们按出现而非按取值计数 (countFo) 并收集 (constantsFo)，这正是常量域上的可判定相等变得不必要的原因；placeFo 把每次出现放到安置所点名的变量处，只走一趟，也不需要弱化引理，而 absFo 把它实例化为名副其实的抽象：按出现次数抬高元数，交出一条无参公式。⊨-abs 认证这笔交易不花含义，⊨-abs₁ 与 asPure₁ 则在「子集被刻出时所用的元数」处把它花掉：可定义子集由一条无参公式在一个参数向量处刻出，且读在可定义幂集据以定义的那套内层语义中。
FOL.Coding：语法作为集合：⌜_⌝ 把构造子序号贴在各部分的码上 (常量编码自身)，而归纳关系 Codes 是接口，使码值不出现在类型检查器必须归一化的等式里。
V.Coding：层级兑现编码的两组参数：数码单射 (#-inj)、Kuratowski 对单射 (pr-inj)，于是 V 上的公式成为 V 的集合。
L.Definability：那一步：Def A，带 A 中参数可定义的 A 的子集之集：语法当索引集，内层满足给含义，本质小性买单；A ∈ Def A 恒成立，传递性下 A ⊆ Def A。
L.Constructible：沿成员递归的塔 Lset，一条方程通吃零、后继与极限；层谓词 isLayer 与 layer-trans；类 isL 与结构 𝒮ʟ。
L.Ordinal：闭包论证所需的序数供给：零、后继、小并皆序数，而 boundingOrd 以单一序数界住任一小族。不含比较，故不花费经典逻辑。
L.Rank：沿成员递归的 von Neumann 秩，取值于层级自身：rank-ord 使它成为以序数进行的度量，rank-fix 认证它为典范索引。
L.Ordinal.Linear：三歧 ord-tri，以及随之而来的 L 侧经典边界：闭包从不需要判定什么，比较则需要，故本章把排中律取作模块参数。
L.Ordinal.Stages：Lset α 中的序数恰是 α 的成员：rank-Lset 与 ord∈Lset→∈ 说无一提前现身，ord∈Lset-suc 说无一迟到。
L.WellOrder.Base：作为束的严格良序 (SWO)，与非空子集的极小元 (leastOf)，经三歧唯一：选择公理将要取用的那件选取装置。反射本来预期是第二个消费方，结果不是，故恰有一个，那就是本书的最后一章 L.Choice.Transversal。
L.Coding.Base：从内部读码：allCodes 把每条无参公式的码汇成一个可命名的集合，而 prAt / tagAt 以有界形式解构 Kuratowski 对与标签，皆 Δ₀ 且适足。
L.Coding.Environment：环境即其图，经 lookup-spec 而函数性；memPairAt 查出一个值，sucAt 认出量词之下的序号移位，seqSet 汇集一个集合上的全部有穷序列。
L.Stage：满足任意序数性质的最小序数，经良基下降得到、经三歧而唯一；包含可构造集的最早阶段是它的头一个实例，已封印，故那次下降永不抵达日后的转换问题。
L.Axioms.Basic：头五个模型字段。外延与正则沿传递性下降；唯一性随即白拿；空集、配对与并则各由一条公式从一个阶段中刻出。finSetL 把配对的论证推广到取自某阶段的任意有穷族，递归的取值表正是这样抵达 L 的。Lset-suc 把后继阶段与前一阶段的可定义幂集认同，正是这一点把那个幂集作为 𝒟ₒS 放进 L。配对那次雕刻也单独陈述为关于塔的事实：pair∈Lset-suc 把一个阶段的两个成员的无序对放进下一个阶段，pr∈Lset-suc 把有序对放到高两个阶段处，而这也正是以有序对写成的任何东西根本得以安置在某个阶段上的原因。
L.Axioms.Separation：Δ₀ 公式的分离与替换，在装下实参与公式全部常元的阶段上；其内容是「属于刻出的集合就是在模型中满足」。
L.Reflect：Montague 的论证，在一个集合之内回答真类大小的存在量词。梯是上升的序数链；若每一级的环境其作答阶段都落在下一级上，则它的极限为自己包含的每个参数元组反射那个存在量词。Single 是单矩阵的梯。取最小阶段而非最小见证，正是把 L 的良序挡在门外的那一手。
L.ReflectFo：整条公式的同一件事，经结构归纳。联合造出的梯一举为公式的每个矩阵作答，而 mkReflect 随即点名一个阶段，公式在其上与它到该阶段的相对化一致：以 Δ₀ 加一个阶段，换下任意的复杂度。
L.Axioms.Numerals：L 之内的数码链，经投影等式钉在层级的数码上。全然构造性，这正是它独立成章的理由：排中律只在收集那一步进入无穷公理。
L.Axioms.Infinity：L 内的数码链，经模型自家配对、并与后继的投影等式，钉在层级的数码上。

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

根，今日陈述，余部完成：

L.Axioms.Full：任意公式的分离与替换，办法是反射那条公式，再把有界的器械施于它的相对化；那个禁闭原子正是使替换的像逃不出阶段的东西。
L.Absoluteness：两门对象语言之间的桥。常元可构造的、关于层级的 Δ₀ 公式，经 liftFo 运进 L 的语言，而 transferFo 说两者说的是同一件事；编码诸章留在层级一侧，从此处被引用。
L.Coding.Model：模型之上的对象语言。「函数」的含义 (prAtL、appAt、svAt、domAt)、取值一侧的对、标签读式、环境，以及 extAt：每条集值子句的写作框架，其两种读法就是它的两个投影。无常元的读式经桥引用；点名数码的读式直接写，因为无界如今免费。
L.Coding.InL：每个码都是 L 的元素，沿构造子的一次归纳，里面什么也没有。正是它使一个码可被点名为模型对象语言的常元，使一族码可充当已内化递归的定义域。全体码之集刻意未证，此处也不需要。另有 closure，一条公式的诸子公式键构成的有穷集；closure-inv 把它读回来；以及 byTag，它把十二个构造子与封闭性谓词提出的八项要求对上一次，而非对上十二乘八次。
L.Coding.Closed：闭包满足对象语言的封闭性谓词，且是满足它的最小者。四个读式的八个实例，再加一次归纳；前者是「对一条公式的诸子码作递归」关于其索引集所需的那条假设，后者是它的取值唯一的理由。那八条子句从不看一条公式，故只对任意可剥开的集合证一次 (Peel：一个成员仅仅是某条公式的键，而那条公式自己的闭包坐落于内)，而 closureClosed 就是 closedOf 落在闭包处、以 closure-inv 充当剥开。此处的一般性免费，因为 byTag 本就是对着任意目标集写的。
L.Coding.EnvSet：落在 L 某集合之上、给定长度的诸环境构成 L 的一个集合，而那正是取补集的诸子句在其中取补的东西。一个小索引类型、一个阶段、一次分离，不用递归。
L.Coding.Sat：给定元语言的一条公式与一个载体，满足它的诸环境之集，沿公式递归造出。没有任何内部的东西：每一步把前几步的集合以常元点名，故每一步只是在周遭集合上作一次分离，而内部诸子句因此成为等式而非定义。只导出十二个取值与它们的成员等式。
L.Coding.Bridge：那个取值是什么。在载体之上的每个环境处，「属于它」就是「在世界 (B, ∈) 中被满足」，而后者正是可定义幂集据以定义的概念；没有这条陈述，从那场递归读出的内部 Def 可证地与任何东西都不相符。右端取内层语义，不取相对化在周遭的读法，因为只有内层那种像那个条件一样对有界量词设两道防。defSet-Sat 把它直接花在 L.Definability 上。登记在案的那份相干性风险没有引爆：把这座桥以内层环境向量为索引之后，量词的扩张就是底族上的前置，于是相干性只剩四条量词子句共享的两条 refl 分支，而带截断的那次恢复被关进「一个成员无非就是一个环境」那条推论里。
L.Coding.Table：诸条目，每条子公式一个；以及递归向它们索取的两件事：每个成员都是一个条目，且键决定它的取值。后者正是花掉码等式单射性的地方，而元数由道路归纳消掉，好让那条等式在它唯一成立的那个元数处使用。此处一切按构造都是模型的元素，因为诸码就是模型自己的。
L.Coding.Sound：那张表满足诸子句，一条一条地。每次验证是四步，其中三步已经造好；剩下的是一条集合等式，而它们便宜，因为元语言的递归当初正是用那条等式所读回的那个条件来定义它的取值的。
L.Coding.Unique：一张在子码封闭的索引上满足十二条子句的表，在每个键处记录的就是递归在那里造出的取值，而正是这一点使那个图单值。对着典范取值陈述，且索引取作变元，因为把键代进一个满足关系里，在任何合理时间内都不会通过类型检查。
L.Coding.Slot：一条公式的递归所索引的那个槽，满足对象语言的封闭性谓词，而那正是满足关系那个图对它的索引集所陈述的假设。是闭包那一章的定理再来一遍，落在模型自己的编码上。
L.Coding.Descent：一场跑在码上的递归如何从一条码走到它的诸部件，而成员关系办不到这件事：Kuratowski 的对把一个部件放在四个成员步之下，而中间那些集合不是码。秩沿成员关系严格增长，故那四步经序数的传递性合成，递归改跑在秩上。
L.Coding.Shape：「是一个码」中封闭性没有说出的那一半。封闭性是八条以标签为键的蕴含，故一个没有可辨标签的成员平凡地满足全部八条；shapedAt 说的是每个成员都是一个带元数标签的对，其标签属于那十二个之一，且载荷是该标签所要求的那种。两个框架承载那十二条，因为十二个标签之间只有两种载荷形状；标签的其余要求是框架所携带的一条关系，而 isTmAt 是其中唯一与公式码无关的那一条。成形性是在两位上陈述的，即那个集合与一个载体，因为一个词项有两样东西要界住，而两者不同：变元的序号由元数数码界住，常元由「属于载体」界住。第二样使一个成员成为该载体之上、而非模型之上某条公式的键，而它写作一位、不写作常元，好让下面的一切都不被重新索引。isTmAt-decode 在任意字母表上把词项还原出来，它是第一个解码，也是唯一一个不需要归纳的；它的常元那一支需要一样谓词供不出的东西，即载体的诸成员就是字母表的像，于是把它取作一条假设。Peel.peel 是两半的会合：形状说出一个成员是十二者中的哪一个并交回它的部件，封闭性说那些部件在该标签所要求的元数上也是成员，而两半各自都不是递归的一步。另一个方向同样欠着，因为一条为了被消费而写下的谓词，在有东西满足它之前什么也没证明：shaped-in 由「每个成员一次选择」造出那个十二重析取，而 closureShaped 把它花在一条公式的闭包上，那正是解码的第一个调用方所欠的第二条假设。一条值得留存的测量：isTmAt 的两个析取支由两条点了名的引理去读，而写成一个函数的两条子句时，本章十分钟内跑不完，因为类型靠推断的分支是对着整个析取、而不是对着它自己那一支求解的。
L.Coding.Recover：解码。在一个于某载体上既封闭又成形的集合里，一个以「某个已言明元数处的键」的形式递交过来的成员，就是该载体之上某条公式的键，而 Decode.recover 把它造出来。字母表是一个参数，目标在它之上陈述，因为消费方以单个载体之上的诸公式为索引，模型之上的公式对它毫无用处。这也使那六个框架更短：在模型之上，每个框架比较码与载荷之前先得把模型的编码搭桥到层级的编码；在字母表之上，码本来就是层级的元素。「每个成员都是这样一个键」此处未予证明，欠这笔账的是造那个集合的人，因为形状对它所绑定的元数分量不加任何条件。递归跑在码的秩上，不跑在码上、也不跑在键上：不跑在码上，是因为成员关系不下降进 Kuratowski 的对；不跑在键上，是因为「对的秩的算术」是一条没人证过的事实。元数作为一个自然数在旁边带着，正是这一点让归纳得以在量词把它抬升到的那个更大的元数上回来；载体则压根不被量化，它是归纳开跑前就已固定的一位。六个框架承载那十二个情形，而每个框架都把自己那个构造子的编码等式作为假设收下，因为构造子若是变元，编码函数便不化简，寻找那条等式的代价就是全部代价。在字母表之上，那十二条等式仍是 refl，因为常量变换按定义与每个构造子交换。
L.Coding.CodeSet：某载体处的诸码，作为 L 的集合，一个落在元数一、一个落在每个元数。smallDom 把诸键装进一个阶段，任意公式的分离再把它们切回来，故本章是两条只差一个合取项的对象语言谓词。共享的那个合取项「仅仅存在一个等于 A 的载体、以及一个在它上面成形的封闭集装着它」是若干无界存在，在此处免费；载体在 hasWitnessAt 里是一位，只在高一层绑定处、即 hasWitness 里，才由 var zero ≐ con A 钉成常元。这样一拆是消费方逼出来的：内部层级把自己的阶段绑定起来，而集合进入公式的唯一方式是被点名，故一条点名了自己载体的谓词，在那层绑定之下压根说不出口。相异的那个合取项说那个成员是第一分量为数码的对，而它之所以存在，是因为 recover 收下实参的形式是某个已言明元数处的键，而 closedAt 与 shapedAt 都不约束元数那一位：形状把它存在量化且不加条件，故那个集合必须从外面把它钉住。isCode 把数码一点名；isCodeAny 把元数绑定，只要求它属于 ωʟ，而读回来无须归纳，因为 ω-specL 是一条等式，且数码链有投影。Codes-spec 与 AllCodes-spec 闭合了两趟往返：一个成员恰是载体之上某条公式的键，分别落在元数一处与某个元数处，故两个集合都是被刻画的，而不是被两条陈述夹住的。全元数那个集合的存在，是为了它所刻画的那一类：对码的递归要在一个码的诸子码处作答，而量词的子公式住在高一级的元数上，一元那一类装不下它，故它当不了定义域。
L.Coding.Satisfaction：那个实例。槽作定义域、图取自上一章，而两半在 funct 处会合：存在性把已经造好的对象递给那个图，唯一性把图所接受的任意一张表对着元语言递归造出的那个钉死。
L.Coding.Uniform：同一个满足关系，跑在某阶段处的诸码之上，而那才是每个消费方想要的定义域：以一条公式的槽为索引，就是一条公式一张表，而消费方到场时手里握着的是一个码、而非「它是其子码」的某条公式。AllCodes 作定义域，而索引集那笔债由成员自己那条公式的槽偿付，其余一概不动，因为那个图把自己的表存在绑定：funct 只需拿出某张装着该成员的合格的表，而最小的一张就是该成员自己那条公式的子公式槽。故 Table、Slot、Sound 与 Unique 都按既有类型施用，而登记在案的那次「在载体与键之对处重新索引」从未发生。唯一新的东西，是把两套编码接起来：层级的编码落在该阶段的字母表之上，模型的编码落在模型的语言之上；用的是 codeBridge (为此而写、至今未用) 加上重标的函子性。val-at 在一个以键的形式给出的成员处读出取值，val-sat 说那个取值就是载体之上的满足关系，而 val-defSet 把它落到元数一处的可定义幂集上。码载体与环境载体保持为彼此独立的参数，只在满足关系有含义之处被钉在一起。每条读式都把成员取作变元、把它的键等式放在旁边，而消费方本会改写的那个名字 keyIn 在它被造出之处封印：一旦把键写开，那个构造就落进一个满足关系里面，而无论证明写多长都展开不了。
L.Coding.Graph：满足关系那个递归的图说了什么。三个存在量词分别管索引集、表与载体，由封闭性、全性与十二条子句设防，取值则从表上读出。一切都被绑定，因为一个图不可以点名一张尚未交给它的表，而那是内化定理唯一禁止的事。一个框架带两个实例，因为那条用来钉住的子句就是框架的参数：satGraphAt 把载体取作一位，供载体本身就是被绑定变元的消费方使用；而 satGraph 把它钉在一个常元上，按它一贯的类型与见证元组交付。
L.Coding.Powerset：可定义幂集在对象语言中、落在一个作为槽位的载体上的描述，也是整条路线为之存在的那一步。内部层级把自己的阶段绑定起来，故一条点名了自己载体的描述在那里压根说不出口；DefAt 什么也不点名。它说的是：u 恰是那些 x 之集，对它们仅仅存在载体之上的一个码 c 与一个取值 v，使得 v 就是满足关系那场递归在 c 处所记录的东西，而 x 是「其单条目环境落在 v 中」的那些载体成员之集。两个存在量词相邻，而这是一次探针逼出的更正：若被一个合取项隔开，码那条假设与满足关系那条假设就落到不同的环境上，于是这条路线会平白背上一条它本来永远用不着的弱化引理。DefinesAt 是单拿出来的第三个合取项，envOneAt 是单条目环境，只有一行，因为长度为一的图只是一个对。DefAt-in 说这个算子满足那条描述，DefAt-out 说别的东西都不满足，后者在 DefOK 之下：描述里的每个存在量词都在 L 上取值，只够得着住在其中的东西，故这条描述恰在「载体的诸可定义子集皆可构造」之处适足。那个旁条件只是消去那一半的假设，因为引入自己的假设已蕴含它；而在一个阶段处，它由后继恒等式一劳永逸地解除，剩下 DefAt-stage：一条真值之间的等式，说这条描述对 𝒟ₒS 成立、对别的什么都不成立。
L.Coding.Sequence：把层级说成一条序列，而这是为它写图时唯一可取的形状。一个图不可以点名它所定义的对象，而塔在某个阶段处是由该阶段以下的塔造出来的，故写下来的改为「逼近是什么」。StepAt 是某个实参处的那一步：一次 extAt 罩住三个相邻的存在量词，即那个实参、逼近在其处所记录的取值，以及它的可定义幂集；最后一样被绑定而不被点名，因为上一章交付的是关于它的一条描述、而不是指称它的一个词项。用一次 extAt 而不用手写的一对包含，因为一对包含会把那三个存在量词复制一份，并把每一种读法拆成互非逆的两半交回来。一个旁条件 PowOK 服务两个方向，因为一个「是 L 的元素」的可定义幂集，也就是一个「诸成员皆可构造」的可定义幂集。ApproxAt 是两个合取项、再无其他：f 恰好定义在那个实参的诸成员上，且它所记录的每个取值都是「在那里、由 f 自身算出的那一步」。它是一条隶属等价、而非一个单向的收集，这使即将到来的那场归纳的动机保持为命题，并把一条内部的函数外延性引理从路线上移除；且它不带单值性合取项，因为步进条件已经把「在一个实参处记录的每个取值」钉住了，故单值性是一条推论，而不是三个置于满足关系之下的全称量词。LsetGraph 把逼近绑定在两者之上。本章的全部代价都出在转换上：两条图读法陈述在具体位上，花掉了 130 秒中的 98 秒；而每一处「假设把环境写开、应用却把它藏在一个缩写背后」，再各花 15 秒。写成两侧是同一个表达式之后，它在两秒之内检查完毕，而这把「变元实参」那条规矩从一次代换推广到一条陈述。
L.Hierarchy：上一章那个图，被对着本书真正造出的那座塔证明，以及用来证明它的那个内部层级。表是有序对之集；它在某个集合上正确，指它在该集合以下所记录的每个取值都是元层面的塔在那里的取值；它完备，指它在以下的每个实参处都记录了一个。step-Lset 从一张正确的表上读出一个被满足的步进、把塔取回来，step-table 则由它写出那一步，而上一章那个旁条件在两者之内一并解除，因为被记录的取值是塔在某个序数处的值，而阶段的可定义幂集可构造。approx-val 是在实参上的一次沿成员的归纳，其动机对一切被记录的取值作量化，故单值性从不作为假设，而 approx-uniq 三行落地。Lset-only 与 Lset-defines 是那个图的两个方向，而 hierL 是后者据以造出的东西：由「序数与塔在它那里的取值」所成之对的集合，经在一个成对的图上作替换而收拢，每个索引的序数性取自 mem-ord 且不加截断，函数性经 mereFunct 偿付。它的规格是一条隶属等价，这使它唯一、也使归纳的动机是命题，而它在被造出之处封印。两次测量，都关乎一个名字：成对的那个图以变元身份进场、随身带着它自己的等式，而不是以那个闭句子的身份进场，价值 85 秒；以及 mem-ord 的那个集合实参必须在每次使用时显式给出，因为 IsOrd 展开成一条带量词的隶属关系、什么也确定不了。本章正是 L 的内部定义的材料，而内部良序就从它上面读出。
L.Axioms.Power：幂集字段，经「界住诸可构造子集、雕出一个阶段」证得。未用凝聚，也不需要：公理索取的是「诸可构造子集构成一个集合」，而非「它们现身得早」。
L.Recursion：L 的集合上，图可表达的函数，其表在 L 中。这是任意公式替换的推论，而非定理：通常那套绝对性纪律是为了让一张表在某个阶段之内可读，而此处没有任何东西在阶段之内读。递归留在它被写下的元语言里；smallDom 为任意小族供给定义域，而 Definition 把一个实例归约为一条定义公式连同它的适足性。witnessInModel 记下图必须遵守的那一条规矩：对象语言的存在量词在 L 上取值，故一个图不可以靠断言被描述者本身存在来描述它。
L.Choice.Stage：L 的一个集合最先在何处拥有成员，而这正是取代 L 的良序的东西。μ 是与它相交的最早阶段，是最小序数算子的一个实例，按 stage 那样封印；meet-suc 使那个阶段成为后继，因为集合进入塔的唯一途径是从它下面那个阶段中被雕出，而 defStage 是它所后继的那个阶段，之所以是函数，是因为在序数之内后继决定它所后继的东西 (ord-suc-inj)。Lset-μ 把首次现身的那个阶段与定义阶段之上的可定义幂集认同，于是一个最先成员带着一个写在单一固定阶段之上的名字，而那正是选取装置所比较的东西。stageBound 是记账所在的序数：在一个集合自身的阶段之上，从而经传递性在它的成员及其成员之上，也在 ω 之上，而诸名字自身正住在那里。此处不陈述 L 上的任何关系，也不跑任何递归。
L.Choice.Finite：有穷诸阶段确是有穷的，且各自带有一个良序。Tally 就是全部的有穷性词汇，即一个命中每个成员的有穷族，既不要求单射，也不要求可判定的相等；powerTally 靠枚举其上的位向量把它抬到可定义幂集上，因为已清点阶段的每个子集都可定义 (finSet∈𝒟ₒ)，而 stageOrder 沿诸数码跑完这一步。precedes 在两个子集最先分歧之处比较它们：非自反性白得，传递性由比较两个见证得到，三歧由排中律连同基底的最小元得到。它的良基性压根不是这个比较自身的性质，且在无穷基底上会失效；它是经 Search 从点名册买来的，即扫过一个有穷族即得任一非空性质的最小元，再由那一步经典推理把它变成可及性。limitOrder 以层号为主键装配 Lset ω，因为按最先分歧处的诸序并不互相延拓，而把层号放在前面就不必延拓；这也是 L.WellOrder.Base 头一回被使唤，且一使唤就是两次，因为层号也在那里被排序。
L.Choice.Name：把后继阶段的成员写下来。一个 Name 是一个元数、一条多一个变量的无参公式，以及一个取自下面那个阶段的参数向量；denote 是它刻出的子集，既读在 Def 据以定义的那套内层语义中 (denote-mem)，也读在已内化的表中 (denote-table)，而 names-complete 说后继阶段的每个成员都有名字。code∈limit 把无参的码放进 Lset ω，因为它由数码与对造成、别无他物，而 code-inj 靠把诸常量抹回去使它忠实。_≺ₙ_ 是写开了的三键字典序比较，先码、再元数、后参数，连同 SWO 的全部四条定律与 leastName，即非空族中最小的名字。
L.Choice.Step：每个阶段一个序，作为一族。birth 是一个可构造集据以被雕出的那个序数，比包含它的最早阶段低一级；它之所以存在，理由正是选取阶段那一章为一格给出的那条：集合进入塔的唯一途径是被雕出。stepAt 是步进，由 Lset δ 上的良序到 Lset (sucV δ) 上的良序，只有一支：处处按最小名字给出，即上一章的三键比较沿一个映射拉回，而那个映射之所以是函数，恰恰是因为下面那个阶段已被良序化。初稿曾在极限阶段以下守着第二支；实测下来它是多余的，而它真正贡献的是一道归一化屏障，opaque 封印以更低的代价给出同样的屏障。pullOrder 沿一个单射搬运良序，是本章写下的唯一一次搬运：步进用它，carry 也用它，即把一个阶段的诸成员表示成命名那一章所取用的那个索引类型。有三个定义与两条读式为外面的调用方说清那个拉回的序是什么：denotesAt，即一个集合的诸名字；IsLeastName，即良序那一章的 IsLeast 架在那一族上，绝不另写一遍 (16 秒对分文不花，因为在算出来的名字处的一次比较会把码之序打开)；leastNameOf，即那场搜寻；以及 stepAt-fill 与 stepAt-read，即那一步对着名字之序读在「调用方已证为最小的任意两个名字」处，且证在封印所在的那条模块序列之内，因为把任一条在顶层重述都要花 39 秒。依值和上的序一概未造。orderAt 就是那一族本身，SWO 的四条定律在每个序数处齐备，沿成员归纳造出，且被封印，因为未封印的序会展开成一场遍历层级的递归。它的比较以诞生阶段为主键，而正因如此 endExtension 分文不花：一次比较从不提到它是在哪个阶段处被读的，故大阶段处的序限制到小阶段上，与那里的序之间是一条路径、而不仅仅是一个等价，唯一要干的活是可构造性与序数性的证明无关性。
L.Choice.Internal：同一个序，用对象语言描述出来，使模型自家的分离能把它雕出来。InLimitAt 是骨架的阶段条件，而它是一个「属于极限阶段」的隶属原子，经 LsetGraphAt 在常元 ωʟ 处说出：无参的码是遗传有穷的，故那场本会从内部判定无参性的递归压根不必写。但它并不是无参性，因为遗传有穷的码可以点名遗传有穷的常量；FreeAt 才是，而它同样是一个隶属原子，落在空字母表处的码集中，所倚的事实是一条无参公式在两个字母表上有同一个码 (freeCode-in、freeCode-out)。读在诸位上 (codeFree-out)，骨架那一位所持有的恰是「比元数多一个变量的诸无参公式」的诸码，而那正是元层面一个名字的公式，codeFree-limit 则由它推出那条阶段条件。NameAt 是落在诸位上的名字，即一个落在极限阶段且不带常量的骨架、一个定义域为元数的载体之上参数序列，以及一个写成单次 extAt 的指称，其条件读的是 satGraphAt 在「由元数与骨架造出的键」处所指派的取值；有两个码集以位的身份抵达它：载体处那一个，没有它，图那张作存在绑定的表什么也钉不住；以及空字母表处那一个，没有它，那个骨架就不是元层面某个名字的骨架。≺At 不跑自己的递归：码用一个对着既有之序的隶属原子，元数用一个数码之间的隶属原子，参数用一次有界字典序量化，而那两个序都以位的身份抵达这条描述。StepAt 是这一族的一步，按最小名字给出，只有一支，故计划当初想要的最小差公式并不需要。order-in 与 order-out 是那两半适足性，落在变元环境的变元位上：只要每个关系位都带着「它持有的是哪个序」这条假设，那条公式对两个名字的数据成立，当且仅当 _≺ₙ_ 对那两个名字成立；参数那个键由一次归纳架桥，把首次相异与命名那一章对向量的递归认同起来。
L.Choice.Table：那个序，由描述变成对象，每个序数处一个。Related 是所实现的那个类，即一个阶段的两个成员所成的、被那里的序所关联的诸对；那次比较是截断着携带的，因为严格良序并不已知是命题值的，而 strict 一举为每一个这样的序把截断脱下来，办法是在消去任何东西之前先按三歧分情形。ApproxAt 与 GraphAt 是逼近与它的图，形状取自 L.Coding.Sequence，但对那条步进条件保持通用；该条件以参数身份取两种形式、只有一个含义进场：落在诸位上，因为图必须绑定它所查阅的那张表；以及落在常元上，因为分离是用单自由变量的公式去雕的。approx-val 靠在实参上的一次沿成员的归纳，把逼近所记录的每个取值钉住，任何地方都没有单值性假设，而 approx-uniq 是那条推论。tableAt 是那个构造，在它被造出之处封印，且与层级那一章不同，它在每个序数处携带两样东西：其以下诸关系的表，经 mereFunct 由替换收拢；以及它那里的关系，从一个界上分离出来，因为阶段处的序没有可供当场拿出的元语言词项。那个界只花一次诉诸，因为一个阶段的两个成员所成的诸对是 L 元素的一个小族，故 smallDom 一举把它们全部禁闭。rel-fill、rel-rep、ixRel-fill 与 ixRel-rep 把任何实现该类的集合的隶属，读在「阶段的成员到场时的两种形状」上，其中第二种正是分离与命名那一章的参数序共同消费的那一种；把它们陈述为「任何实现该类的集合」，正是使它们比那个构造早一个阶段可用之处，而命名那套机器要的就是那里；relL-fill、relL-rep、ix-fill 与 ix-rep 则是那四条在本章所造的集合处的实例。留待解决的是那条步进条件自身的适足性，即上一章的 StepAt 对着元层面那一步，此处以 Described 的两条假设之名点出。
L.Choice.Faithful：把描述做成忠实的，并把那个框架的两条假设解除到只剩一条。BirthAt 是诞生阶段在对象语言中的说法，它不点名任何常元，也不需要后继运算：那一位处的塔不装这个集合，而那座塔的可定义幂集装它，而 Lset-suc 使这两条等价于「比包含它的最小阶段低一级」，且只花在元层面一侧。BirthAt-out 与 BirthAt-in 是它落在变元位上的两条读式，唯一的假设是序数性，其中可靠性是一次对着最小阶段的三歧分情形，写成一个具名辅助。isCodeAnyAt 是任意元数处、落在一位所持载体上的码谓词，而它是实例化、不是构造：元数绑定那个合取项与见证那个合取项都早已存在，新的只是它们的会合；CodesAt 是它们雕出的那个集合，一次 extAt，其两条读式把那一位钉在该载体之上的码集上，于是命名描述的码集那一位由描述钉住、而不由外部的一条等式钉住。order-unfold 是序之族在一个阶段处的定义方程，即在递归的计算规则上作的一次 cong；bornIn 是 birth-in 的逆，它为这条描述省下一层绑定；stepMoved 沿载体之间的一条等式搬运一次步进比较，是就地重建、而不是伸手去另一个模块里够。CondCore 是阶段处的序被完整描述出来，以诞生阶段为主键，对步进条件保持通用：它绑定四个集合，把阶段取作词项，使得常元那一形式不花绑定，且在被造出之处封印。Cond、Cond₀、cond-spec 与 cond₀-spec 是上一章那个框架所索取的两种形式连同它们的含义，于是 Described 可以施用，它所证的一切都可取用，条件只有那个步进参数、别无其他。本章记下四条实测，因为每一条都是定律、不是偏好：诞生描述所满足于其上的那两个元素必须封印 (178 秒对 2 秒)、环境必须写全而不可缩写 (207 秒对 3 秒)、结论落在满足关系上的两路分情形必须是具名辅助而绝不可用 with (超过 300 秒)、以及读在诸常元上的描述必须在被造出之处封印 (每条读式 160 秒)。不在此处的，是那一步自身的适足性，即 L.Choice.Internal 的 StepAt 对着 stepAt，它以参数 Stp 的身份进场，stp-out 与 stp-in 是它的含义：前者取用表在该载体处所记录的每一个取值上的正确性，因为它所读的那条条件可能自己绑定了一个取值；后者取用「实现那里的序」的单个取值，因为那正是它要塞进去的东西。
L.Choice.Adequate：那一步自身的适足性，对着命名那一章的比较。paramSeq-in 与 paramSeq-out 是参数那个合取项的两个方向：载体之上的一个向量，就是它之上一个定义域为元数的环境；而任何这样的环境都能被读回成一个向量，且不带截断，因为某个序号处的条目是命题，而一个取值的索引是一条纤维，故一分有穷选择也不花。envAt、numAt、keyAt 与 valAt 是指称那个合取项所满足于其上的四个元素，在被造出之处封印；codeEl 与 envEl 是另外两个，供最小名字描述所携带的那个全称使用。Named.Body.denote-fill 与 Named.Body.denote-read 是指称的两个方向，长四环：扩张后的环境是被推到诸参数前面的那个成员，它的长度是元数加一，键是那个长度与骨架之对，而图在那里的取值就是载体之上的满足关系。NameAt-fill 与 NameAt-read 把五个合取项装配成一个元层面名字、又拆回来；Least.Min.LeastAt-fill 与 Least.Min.LeastAt-read 对最小名字做同样的事，那个全称在「一个名字自己的三样数据」处实例化；而 Least.Step.StepAt-fill 与 Least.Step.StepAt-read 是那一步，即两个最小名字加一次比较。leastPin 靠最小元的唯一性，把「这条描述称作最小」的那个名字与 leastName 交回的那个认同起来。这一切都站在上一章留下的那个框架里：每个关系位都带着「它持有的是哪个序」这条假设。三次实测，每一条都是在新地方遇上的旧规矩：适足性等式的复合无法由「对着写出来的类型」的一次代换交割，任何实参都不行、变元也不行 (denote-table 400 秒跑不完，而它的两个因子 denote-mem 与 val-sat 各自 2.4 秒交割)，故复合逐因子消费；六层绑定那一块要求它的环境被写开，不可用 where 缩写 (超过 400 秒对 20 秒)；而六重存在的载荷经 StepOf 读出，绝不经手写的 Σ。在 L.Choice.Table 的结果成为无条件之前仍然缺席的东西，本章据实点名：那个框架里为诸码所设的关系位，要的是作为 L 之元素的 limitOrder，而至今无人造出它。
L.Choice.Limit：极限阶段诸成员上的序，作为 L 的一个元素，而这正是内化那个框架里为诸码所设的位一直索取的东西。LevelAt 是层号在对象语言中的说法，三个合取项，且除 ω 外不点名任何常元：那一位持有 ω 的一个成员、那里的塔装着这个集合、而没有更小数码的塔装它。两条读式都站在变元位上，而层号以变元数码的身份到场、携带它自己的定义等式，这正是 145 秒与 1.8 秒之差，因为层号是一场经典可及性递归，而槽位处的转换检查把它撬开。PrecedesAt 是最先分歧处那次比较的单独一步，其中不含任何具体之物：基底关系与基底阶段被握在槽位里，故这条描述能站在「关系是某场递归之取值」的地方；而基底关系的那次隶属经 appAt 抵达，因为对是被描述的、不是被点名的。strictLimit 先按三歧分情形，把一次比较上的截断脱下来。LimitOrdAt 把两个键接成一个析取，第一支绑两个层号并按隶属比较它们，第二支绑一个，于是层号之间的等式根本不进对象语言。pairsBound 经 smallDom 把那个序可能关联的每一个对都禁闭起来，而 codeOrder 是从它上面分离出来的、在造出之处封印；codeOrder-fill 与 codeOrder-rep 是两条表示引理，而 CodeKeys.AtParams 就是 Adequacy.Keys，其为诸码所设的位由它们填上，实参相同，中间不设转接。这一切都以一条假设为条件，即 BeforeAt 连同它对着 before 的两条读式，也就是沿诸数码的那族最先分歧之序在内部的说法：一场取值为关系的递归，故要说的是逼近；它比塔便宜，因为索引是 ωʟ 的成员，而那一步已经写好。两次实测，每一条都是在新地方遇上的旧规矩：一次分情形，若其被检者是某个束的比较、而其结论是一个满足关系，就跑不完，而写在一个显式的和上、诸支具名，则不花分文 (超过 300 秒对 2.4 秒)；以及那条接合起来的描述必须在造出之处封印，因为分离的那条条件会在两层绑定之下把它展开 (超过 300 秒对 2.7 秒)。
L.Choice.Before：最先分歧之序的那一族，内化，它兑现了上一章赖以立足的那条唯一假设。relAt 是每个数码处的那个关系，作为 L 的一个元素，即在那个有穷阶段的诸对之上、用上一章那条步进描述雕出的一次分离，而那条描述的两个槽位被绑定、并用对象等词钉在诸常元上，于是一条描述同时服务于那次分离与那个图；relAt-out 与 relAt-in 是它的两条读式，对数码作归纳一并证出，每个方向都在前趋处花掉另一个，因为上一个关系只在一致性子句内部被查阅，而 precedes-map 反变地搬运那次比较。RelBodyAt 是那一步，对成员、索引与逼近保持通用，其中前趋说成索引的 ∈-极大成员，故不需要对象等词，而那一步恰好在这场递归为空之处 (零处) 为空。RelStepAt、ApproxAt 与 RelGraphAt 照 L.Coding.Sequence 而来，不带单值性合取项；step-rel 与 rel-step 是通往元语言的那座桥，approx-val 靠一次良基归纳把逼近所记录的每个取值钉住、且单值性在任何地方都不是假设，而 rel-only 是那个图的确定性。approxSet 是当场拿出来的那个逼近，根本不花任何公式，因为某个数码以下的逼近是有穷的，只要 smallStage 把它的诸成员放进同一个阶段，finSetL 就把它张出来；beforeFam 是那一族，沿 ωʟ 的一次替换，在造出之处封印，而它的两个方向陈述成对着这场递归、不对着任何公式。BeforeAt 在某个槽位所持的数码处读出那一族，其中在常元处的应用用 appAtC，而被比较的那两个集合不加禁闭；有了它，Described 便被实例化，于是 codeOrder 与 CodeKeys 是无条件的。一次实测，本部最大的一次：四条描述必须在造出之处封印，因为不封印时，每一次在具体环境上的满足关系都要把一条内部装着两份完整层级描述的公式正规化 (376 秒对 3.8 秒，九十九倍)；而造出那一族的那个框架在高一层遵守同一条定律，办法是交回一个其中不出现任何公式的三元组。
L.Choice.Order：那一步被描述出来，序之表随之变成无条件的。Stp 就是那条描述：一条被封印的公式，绑定六个集合并钉住两个常量。六个是：阶段处的塔，经 L.Coding.Sequence 的 LsetGraphAt 抵达；它的可定义子集，经 L.Coding.Powerset 的 DefAt 抵达，并要求被比较的那两个集合落在其中，那一步的两个隶属分量就是这样到场的，而不必动用谁也没有的一条引理；表在该阶段的取值，经 appAt 抵达，正是这一点使那条描述始终读在调用方所持的任意一张表上；以及塔之上的码集，经 L.Choice.Faithful 的 CodesAt 抵达，而那条描述当初就是为这个槽位写的。用对象等词钉住的两个是 L.Choice.Limit 的 codeOrder 与空字母表处的码集，因为槽位持有变元，而那两样是特定的集合。落在那七个槽位上的主体就是 L.Choice.Internal 的 StepAt。Slots 供给那一步的适足性的全部六个实参，对那六个集合保持通用、以它们的等式为假设：码那一侧由极限与族两章无条件给出，载体那一侧由 L.Choice.Table 在所绑定取值处的诸读式给出，而那正是步进参数自己的假设，也是从外面取的唯一输入。stp-out 与 stp-in 是对那六个绑定的拆开与装回，与 L.Choice.Adequate 的诸步进读式及 L.Choice.Step 的两条复合而成，且它们承接了框架的那份不对称：可靠性对表在那里记录的每一个取值作全称，完备性取的是调用方据以实现的那单个取值。随后一行打开 L.Choice.Faithful.Ordered，整张表随之变成无条件的：CondCore、Cond、Cond₀ 连同它们的两条规格，以及出自 L.Choice.Table 的 StepAt、ApproxAt、GraphAt、approx-val、graph-only、graph-table、tableAt、relL、relL-spec 与全部四条表示引理。一次实测，一条定律在新地方的现身：一个框架所结论于其中的类型，要在它被造出之处封印，因为把那个框架实例化到描述所绑定的具体元素上会把它正规化，而不封印时那件事跑不完 (超过 200 秒，对全章的 7 秒)。Bound 是最后一章据以分离的那个形状：L 的一个集合的界层序数、那里的塔的诸成员上的序作为模型的一个元素，以及它的两条表示引理。
L.Choice.Transversal：选择，以及前沿清空。公理取模型 record 陈述它时所用的横截形式：成员非空且两两不交的集合，有一个与它每个成员恰交于一点的集合。全程不用 L 的良序，因为此处根本没有；集合是小的，故 L.Choice.Stage 的界层序数一举装下该族、它的成员与它们的成员，而 L.Choice.Order 的 Bound 供应那里的塔上的序作为模型的一个元素。Pick 是那条描述，一个自由变元与两个常量：该族的某个成员含有这个集合，且那个成员中没有任何东西排在它之前；那个序用对象等词钉在一个槽位上，因为「一个对属于某个关系」这条原子是从槽位取那个关系的。pick-in 与 pick-out 是它对着 L.WellOrder.Base 的 IsLeast 的两条读式，每个截断载荷都有名字。transversalSet 是模型自家的分离据它在那座塔之上雕出的东西，而 transversal 数清它与每个成员之交：存在性来自 leastOf，即那场自写下之日起一直没有消费方的极小元搜索；唯一性来自两两不交，而全书别无他处用到它，经 isPropLeastOf 得出。对所供给的那个 ZF 模型的依赖，只是沿交的规格的一次搬运。hasChoiceL 就是模型的选择字段，于是登记簿清空，L.Frontier 连同根章的第二个参数一并删除。一次实测，且是一条定律偏偏没有咬人：读在常元上的描述要在被造出之处封印，这条定律在被发现之处值九十九倍，在此处则一文不值 (封印与否都是 2.3 秒)，因为这条描述不携带任何已编码的语法；封印仍然保留，而那个数字被记下来，因为这条定律关乎的是一条描述装着什么。
L.Model：根章：诚实的相对一致性表述；外延与正则沿传递性下降；L⊨ZF 与 L⊨ZFC 合龙，唯一假设是排中律。本章曾以第二个参数收下的债务登记簿 L.Frontier 已不复存在：它开张十一个字段，缩过六次，随着清空它的那一章一并删去。

import L.Model

候用的工具

这几章至今在主干上没有任何消费者；它们的首批消费者随第四部的深层机器到来，读在靠后，好让主线不断。

FOL.Manipulation.Renaming：变量变换，本书全部的变量演算：语法上的 renameFo，与一条通吃弱化、交换、收缩的正确性定理 ⊨-rename。
FOL.Manipulation.Relativize：把无界量词收紧到常量界，Δ₀ 见证随附，并给出正确性等式。

import FOL.Manipulation.Renaming
import FOL.Manipulation.Relativize