Landmarks

奖杯陈列室，而且是故意摆在入口处的。下面每座地标都以一条自足的签名重述本书的一项里程碑定理，假设账单全额陈列，并指认证明它的章节。初读时这里的一切都不指望被看懂：这些签名就是目的地，而学会逐个符号、逐条假设地读懂它们，正是全书其余部分的任务。每读完一部，请回到这里。对回访的读者，地标是稳定的锚点：论文可以直接引用，而不必关心其证明住在书中何处。

{-# OPTIONS --cubical --safe --guardedness #-}

module Landmarks where

open import Base.Prelude
open import Base.Impredicativity using ( Impredicativity )
open import Base.Classical using ( LEM )
open import Base.Choice using ( SetChoice )
open import V.Hierarchy using ( 𝒮ᵥ )
open import FOL.ZFModel using ( isZFModel; isZFCModel )
open import L.Constructible using ( 𝒮ʟ )
import V.Model
import L.Model

层级满足 ZF(C)

主打名是经典版：给定模型自身真值层上的一份排中律，累积层级是 ZF 的模型 (章节 V.Model)。其精确价格版以后缀携带假设，只收第零部的非直谓性打包；再经 Diaconescu 定理 (章节 Base.Choice)，一份集合层选择就资助到 ZFC。

V⊨ZF : ∀ {ℓ : Level} → LEM (ℓ-suc ℓ) → isZFModel (𝒮ᵥ {ℓ})
V⊨ZF = V.Model.V⊨ZF

V⊨ZF-impredicative : ∀ {ℓ : Level} → Impredicativity ℓ → isZFModel (𝒮ᵥ {ℓ})
V⊨ZF-impredicative = V.Model.VModel.V⊨ZF-impredicative

V⊨ZFC : ∀ {ℓ : Level} → SetChoice (ℓ-suc ℓ) → isZFCModel (𝒮ᵥ {ℓ})
V⊨ZFC = V.Model.V⊨ZFC

可构造宇宙满足 ZFC

本书的主定理 (章节 L.Model)：给定模型真值层上的一份排中律，可构造结构满足 ZFC。一个假设，而它与上一座地标所付的是同一个。这条签名在全书大半光景里还带第二个参数，即余部尚欠陈述的登记簿；如今登记簿已空，那个参数也已消失。与上一座地标合读，这就是选择公理相对一致性的语义形式：ZF 宇宙的体内携带着一个 ZFC 子宇宙。

L⊨ZFC : ∀ {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) → isZFCModel (𝒮ʟ {ℓ})
L⊨ZFC = L.Model.L⊨ZFC