Bedrock沿公式递归构造满足关系
可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。
阅读指南 · 依赖地图给定 L 中的集合 B 和一条公式，我们构造 B 上满足该公式的环境所组成的集合。构造沿公式递归进行：复合公式的集合由其直接子公式的集合确定，而原子与假则被直接处理。无论哪种情形，集合都由分离得到：从「B 上长度 n 的全部环境」这个集合中，保留条目满足描述条件的那些。所得集合的隶属等式逐一描述十个公式构造子。
递归沿元语言的公式进行，这一点决定了每个步骤的形状。Agda 可以检查这条公式，因此每一步都能把子公式处已产出的集合作为描述条件的常元点名，而对象语言始终不必对码作量化；于是每一步都只是一次分离。原子情形也相应简短：元语言的词项一眼可辨是变元还是常元，读取其取值只需一种情形，而非码化子句必须区分的两种。
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Classical using ( LEM ) module L.Coding.Satisfaction {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
构造假设模型层级的后继处成立排中律。所处理的是集合论语言的公式，包含相等、隶属、三个二元联结词、假，以及有界与无界量词。
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Term; con; var; Formula ; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ ) import FOL.Absoluteness
满足关系将在累积层级的可构造子结构中读取。公式绝对性提供这种限制结构中的读法，有序对则编码充当环境的图。
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
对每条公式，分离从编码环境集里截出其满足集合。公式 appAt 与 consAtL 分别描述环境图中的查找和添入一个值后的扩展；envSet 给出所需长度的全部环境。
open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate ) open import L.Coding.Expressions {ℓ} using ( consAtL; numL ) open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet )
存在子句给出命题截断下的见证。有限指标先化为自然数，再由层级内部的冯·诺伊曼数码表示。
open import Cubical.Data.FinData using ( toℕ ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁; ∥_∥₁; squash₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
层级的数码构造把这些指标命名为集合。打开可构造的真值结构后，本章中的隶属与满足便有了固定含义。
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( #_ )
下文的 _⊨_ 表示限制可构造结构中的满足关系，并在有限环境向量下求值。
open hPropStructure 𝒮ʟ module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
变元与常元的求值
变元从环境中取得其索引处的值；常元则直接指称自己的值。这两件事实必须在对象语言内部说出，因为描述条件本身是公式。词项读式 tmIs 说的是：在取值槽位与环境槽位之间，环境把该词项对应到取值槽位中的那个值。对常元，这就是取值槽位与常元之间的等式本身。对变元，这是一条存在陈述：载体的某个元素等于该索引的数码，而应用子句说，这个索引与所记录取值组成的对属于环境槽位处所记录环境的图。全章的满足判断都在 L 中读出。
private nn : ℕ → S nn k = # k , numL k
内部数码把外围的冯·诺伊曼数码连同其可构造性证明配成对，于是索引在需要之处总能在 L 内部被点名。
tmIs : ∀ {n m} → Term S n → Fin m → Fin m → Formula S m
读式取一个词项、持有该词项取值的槽位、以及读取词项时所处环境的槽位，返回该长度环境上的一条公式。
tmIs (var i) v e = ∃̇ ((var zero ≐ con (nn (toℕ i))) ∧̇ appAt (suc e) zero (suc v))
对变元，子句说：载体的某个元素 x 等于该索引的数码，且「这个索引与取值槽位处的取值组成的对属于环境槽位处所记录环境的图」。等式只是钉住索引见证；携带内容的是应用子句。
tmIs (con c) v e = var v ≐ con c
对常元，无须考察环境：取值槽位就等同于该常元。
tmIs-var-in : ∀ {n m} (i : Fin n) (γ : S ^ m) (v e : Fin m) → ⟨ pr (# (toℕ i)) (fst (lookup v γ)) ∈ fst (lookup e γ) ⟩ → ⟨ γ ⊨ tmIs {n} (var i) v e ⟩
充分性的两条引理把公式与它所编码的外围隶属连接起来。向内：若槽位 e 处的环境包含数码 i 与槽位 v 处取值组成的对，则 γ 满足这条读式。
tmIs-var-in i γ v e h = ∣ nn (toℕ i) , ( refl , subst ⟨_⟩ (sym (appAt-adequate (suc e) zero (suc v) (nn (toℕ i) ∷ γ))) h ) ∣₁
见证就是数码本身；其定义等式是定义性的，而那份隶属沿充分性路径反方向传输，从外围陈述变为扩展环境上的内部子句。
tmIs-var-out : ∀ {n m} (i : Fin n) (γ : S ^ m) (v e : Fin m) → ⟨ γ ⊨ tmIs {n} (var i) v e ⟩ → ⟨ pr (# (toℕ i)) (fst (lookup v γ)) ∈ fst (lookup e γ) ⟩
向外，读式的满足给出外围隶属。这里首次出现本章的一条一般原则：只要目标是命题或截断，截断见证即可消耗；下文任何地方都不违反这一点。
tmIs-var-out i γ v e = PT.rec (snd (pr (# (toℕ i)) (fst (lookup v γ)) ∈ fst (lookup e γ)))
截断的见证由条目 x 与两份证明组成：x 是该索引的数码，且扩展环境上的子句成立。
(λ { (x , (qx , m)) → subst (λ w → ⟨ pr w (fst (lookup v γ)) ∈ fst (lookup e γ) ⟩) qx (subst ⟨_⟩ (appAt-adequate (suc e) zero (suc v) (x ∷ γ)) m) })
充分性路径把该子句等同于 x 与取值组成的对的隶属；沿其等式把 x 改写回数码，剩下的恰是向外方向所应交付的那份隶属。
满足公式的环境集
对每个构造子，一条公式描述分离时应保留哪些环境，而每条描述条件都是定义在该公式自身元数的环境上的一条单变元公式。联结词引用为子公式已构造的集合，把它们作为常元点名。无界量词把载体的一个成员添加到环境之前，再检验扩展是否属于元数多一的那个集合；有界量词再加一道约束：新条目须落在界项的取值之中。于是构造的每一步都只是一次分离。
private opaque sep : (a : S) → Formula S 1 → S sep a φ = hasSeparationL a φ .fst .fst
分离被一次性记录在不透明的包装之中：从一个集合与一条单变元公式产出子集。
sep-mem : (a : S) (φ : Formula S 1) (x : S)
→ (x ∈ˢ sep a φ) ≡ ((x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ))
sep-mem a φ = hasSeparationL a φ .fst .snd
隶属规格就是分离的全部内容：属于子集，等于属于外围集合并且满足条件。
module _ (B : S) where cond : ∀ {n} → Formula S n → Formula S 1
固定基集合 B。每条公式都确定一个关于 B 上编码环境的一元条件；从全部环境中分离出满足该条件者，便得到这条公式的满足集合。
Sat : ∀ {n} → Formula S n → S Sat {n} φ = sep (envSet B n) (cond φ)
满足公式的环境集，就是从该公式元数的完整环境集中分离出满足条件的环境所得。
Sat-mem : ∀ {n} (φ : Formula S n) (x : S) → (x ∈ˢ Sat φ) ≡ ((x ∈ˢ envSet B n) ⊓ ((x ∷ []) ⊨ cond φ)) Sat-mem {n} φ = sep-mem (envSet B n) (cond φ)
它的隶属等式恰记录了两项要求：该环境有正确的元数与取值，并且满足这条公式特有的条件。
cond (t ∈̇ u) = (∃̇ (∃̇ ( tmIs t (suc zero) (suc (suc zero)) ∧̇ ( tmIs u zero (suc (suc zero)) ∧̇ (var (suc zero) ∈̇ var zero) ))))
隶属原子绑定两个条目，并断言对象语言的隶属：在槽位 suc zero 处读取的 t 的取值，属于在槽位 zero 处读取的 u 的取值。两个取值都对照环境槽位读取。
cond (t ≐ u) = (∃̇ (∃̇ ( tmIs t (suc zero) (suc (suc zero)) ∧̇ ( tmIs u zero (suc (suc zero)) ∧̇ (var (suc zero) ≐ var zero) ))))
相等原子形状相同，只是把隶属换成了相等。
cond (a ∧̇ b) = ((var zero ∈̇ con (Sat a)) ∧̇ (var zero ∈̇ con (Sat b)))
合取的条件要求该环境同时属于两个子公式集合，二者都以常元点名。
cond (a ∨̇ b) = ((var zero ∈̇ con (Sat a)) ∨̇ (var zero ∈̇ con (Sat b)))
析取的条件要求至少属于二者之一。
cond (a ⇒̇ b) = ((var zero ∈̇ con (Sat a)) ⇒̇ (var zero ∈̇ con (Sat b)))
蕴涵的条件说：属于前件集合蕴含属于后件集合。
cond ⊥̇ = ⊥̇
假的条件就是假本身：没有环境满足它。
cond (∃̇ a) = (∃̇∈ (con B) (∃̇ ( consAtL zero (suc zero) (suc (suc zero)) ∧̇ (var zero ∈̇ con (Sat a)) )))
无界存在量词在载体上取值：B 的某个成员 x 扩展环境，扩展子句证明新的列表确是环境，而扩展后的环境属于子公式的集合。
cond (∀̇ a) = (∀̇∈ (con B) (∀̇ ( consAtL zero (suc zero) (suc (suc zero)) ⇒̇ (var zero ∈̇ con (Sat a)) )))
无界全称是它的对偶：载体的每个成员一经添加，扩展后的环境就落入子公式的集合。
cond (∀̇∈ t a) = (∀̇ ( tmIs t zero (suc zero) ⇒̇ ∀̇∈ (con B) ( (var zero ∈̇ var (suc zero)) ⇒̇ ∀̇ ( consAtL zero (suc zero) (suc (suc (suc zero))) ⇒̇ (var zero ∈̇ con (Sat a)) ) ) ))
有界全称分三层量化。最外层从自己的槽位读出界项的取值 w；对每个这样的 w，量化载体成员 x，并加上 x ∈ B 与 x ∈ w 两道约束；再对每个 x，要求由 x 扩展环境所得的 e' 经扩展子句认证后属于子公式的集合。这里 w 只是界的辅助槽位；子公式 a 的环境是 e'，它恰好给环境增加一个条目。
cond (∃̇∈ t a) = (∃̇ ( tmIs t zero (suc zero) ∧̇ ∃̇∈ (con B) ( (var zero ∈̇ var (suc zero)) ∧̇ ∃̇ ( consAtL zero (suc zero) (suc (suc (suc zero))) ∧̇ (var zero ∈̇ con (Sat a)) ) ) ))
有界存在把同样的三层写成存在陈述：先读出界项的取值，见证是载体中落在该取值之内的成员，且其扩展环境属于子公式的集合。基与界两道约束都得到保留。
条件的读取
一般等式 Sat-mem 把「属于环境集」与「满足条件」分开。合取、析取、蕴涵与假可直接按 cond 的定义归约，无须辅助等价。下面的引理只处理其余情形：展开两个原子存在式与存在量词所隐藏的见证，或读出全称量词提供的函数。它们只讨论 cond φ 的满足；环境集合取项仍留在 Sat-mem 中。
CondAtom : ∀ {n} → Term S n → Term S n → (S → S → Type (ℓ-suc ℓ)) → S → Type (ℓ-suc ℓ) CondAtom t u R z = Σ[ v ∈ S ] (Σ[ w ∈ S ] (⟨ (w ∷ v ∷ z ∷ []) ⊨ tmIs t (suc zero) (suc (suc zero)) ⟩ × (⟨ (w ∷ v ∷ z ∷ []) ⊨ tmIs u zero (suc (suc zero)) ⟩ × R v w)))
对两条原子，条件是一条存在陈述，其展开形状就是 Σ 类型 CondAtom：t 的取值 v、u 的取值 w，二者都经词项读式对照 z 处的环境读取，外加两个底层集合之间的关系 R。该类型本身不带截断；截断的形式出现在下面的各条辅助引理处。
cond∈-in : ∀ {n} (t u : Term S n) (z : S) → ∥ CondAtom t u (λ v w → ⟨ fst v ∈ fst w ⟩) z ∥₁ → ⟨ (z ∷ []) ⊨ cond (t ∈̇ u) ⟩ cond∈-in t u z = PT.map (λ { (v , (w , r)) → v , ∣ w , r ∣₁ })
隶属的向内映射把截断的三元组重新包装成两个量词所期待的嵌套见证。消去之所以合法，是因为目标本身作为外层截断就是命题，而与内部关系具有何种性质无关。
cond∈-out : ∀ {n} (t u : Term S n) (z : S) → ⟨ (z ∷ []) ⊨ cond (t ∈̇ u) ⟩ → ∥ CondAtom t u (λ v w → ⟨ fst v ∈ fst w ⟩) z ∥₁ cond∈-out t u z = PT.rec squash₁ (λ { (v , hv) → PT.map (λ { (w , r) → v , (w , r) }) hv })
向外映射把嵌套的见证摊平回三元组，整个论证都留在截断之内。
cond≐-in : ∀ {n} (t u : Term S n) (z : S) → ∥ CondAtom t u (λ v w → fst v ≡ fst w) z ∥₁ → ⟨ (z ∷ []) ⊨ cond (t ≐ u) ⟩ cond≐-in t u z = PT.map (λ { (v , (w , r)) → v , ∣ w , r ∣₁ })
相等原子携带的关系是 fst v ≡ fst w，即底层集合的相等；其向内映射与隶属情形逐字相同。
cond≐-out : ∀ {n} (t u : Term S n) (z : S) → ⟨ (z ∷ []) ⊨ cond (t ≐ u) ⟩ → ∥ CondAtom t u (λ v w → fst v ≡ fst w) z ∥₁ cond≐-out t u z = PT.rec squash₁ (λ { (v , hv) → PT.map (λ { (w , r) → v , (w , r) }) hv })
其向外映射也与隶属情形相同，只是交换了关系。
CondQuant : ∀ {n} → Formula S (suc n) → S → Type (ℓ-suc ℓ) CondQuant a z = Σ[ x ∈ S ] (⟨ fst x ∈ fst B ⟩ × (Σ[ e' ∈ S ] (⟨ (e' ∷ x ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc zero)) ⟩ × ⟨ fst e' ∈ fst (Sat a) ⟩)))
对无界存在量词，展开后的条件是 Σ 类型 CondQuant：基的一个成员 x、经扩展子句认证为「环境 z 添加 x 后的扩展」的条目 e'、以及 e' 属于子公式集合的隶属。该类型同样不带截断，截断在辅助引理处添加。
cond∃-in : ∀ {n} (a : Formula S (suc n)) (z : S) → ∥ CondQuant a z ∥₁ → ⟨ (z ∷ []) ⊨ cond (∃̇ a) ⟩ cond∃-in a z = PT.map (λ { (x , (x∈ , (e' , r))) → x , (x∈ , ∣ e' , r ∣₁) })
向内映射把扩展数据折进存在量词自身提供的那一个截断见证之中。
cond∃-out : ∀ {n} (a : Formula S (suc n)) (z : S) → ⟨ (z ∷ []) ⊨ cond (∃̇ a) ⟩ → ∥ CondQuant a z ∥₁ cond∃-out a z = PT.rec squash₁ (λ { (x , (x∈ , hv)) → PT.map (λ { (e' , r) → x , (x∈ , (e' , r)) }) hv })
向外依次展开两层嵌套的截断见证；两个目标都是截断、因而是命题，展开因此合法。
cond∀-in : ∀ {n} (a : Formula S (suc n)) (z : S) → ((x e' : S) → ⟨ fst x ∈ fst B ⟩ → ⟨ (e' ∷ x ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc zero)) ⟩
对每个允许的取值及其经过认证的扩展，前提给出该扩展属于子公式的满足集合。
→ ⟨ fst e' ∈ fst (Sat a) ⟩) → ⟨ (z ∷ []) ⊨ cond (∀̇ a) ⟩ cond∀-in a z k x x∈ e' hc = k x e' x∈ hc
对无界全称，展开后的条件是一个函数：给基的每个成员连同其扩展，指派子公式在该扩展处的真值。向内与向外是同一个函数沿量词两个方向的读法。
cond∀-out : ∀ {n} (a : Formula S (suc n)) (z : S) → ⟨ (z ∷ []) ⊨ cond (∀̇ a) ⟩ → ((x e' : S) → ⟨ fst x ∈ fst B ⟩
向外读取条件时，保留取自 B 的值，以及把该值添入后得到的环境。
→ ⟨ (e' ∷ x ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc zero)) ⟩ → ⟨ fst e' ∈ fst (Sat a) ⟩) cond∀-out a z h x e' x∈ hc = h x x∈ e' hc
这里不出现截断，因为全称的满足靠给出验证者来完成，而两个方向做的恰是这件事。
CondBnd : ∀ {n} → Formula S (suc n) → S → S → Type (ℓ-suc ℓ) CondBnd a z w = Σ[ x ∈ S ] ((⟨ fst x ∈ fst B ⟩ × ⟨ fst x ∈ fst w ⟩) × (Σ[ e' ∈ S ] (⟨ (e' ∷ x ∷ w ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc (suc zero))) ⟩ × ⟨ fst e' ∈ fst (Sat a) ⟩)))
有界量词多出一层。条件依次量化：界项的取值 w、落在 w 中的基成员 x、以及环境 z 添加 x 后的扩展 e'，后者由扩展子句认证，并要求属于子公式的集合。w 的角色是辅助性的：它承载界的取值，而子公式 a 的环境是 e'，后者恰给环境 z 增加一个条目，即成员 x。
cond∃∈-in : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S) → ∥ (Σ[ w ∈ S ] (⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩ × ∥ CondBnd a z w ∥₁)) ∥₁ → ⟨ (z ∷ []) ⊨ cond (∃̇∈ t a) ⟩
有界存在把见证叠放起来：外层截断针对界项的取值 w，其内是 CondBnd a z w 的内层截断，装着载体成员及其扩展。
cond∃∈-in t a z = PT.map (λ { (w , (hw , hx)) → w , (hw , PT.map (λ { (x , ((x∈B , x∈w) , (e' , r))) → x , (x∈B , (x∈w , ∣ e' , r ∣₁)) }) hx) })
第一个 PT.map 消去 w 上的外层截断，嵌套的 PT.map 消去 CondBnd 的内层截断，把成员与扩展折进存在量词自身的量词之中。两个目标都是截断、因而都是命题，两次消去的合法性同出一源。
cond∃∈-out : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S) → ⟨ (z ∷ []) ⊨ cond (∃̇∈ t a) ⟩ → ∥ (Σ[ w ∈ S ] (⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩ × ∥ CondBnd a z w ∥₁)) ∥₁
向外陈述暴露出同样的两层形状：外层是界项的取值，其内是截断的「载体成员及其扩展」之记录。
cond∃∈-out t a z = PT.map (λ { (w , (hw , hx)) → w , (hw , PT.rec squash₁ (λ { (x , (x∈B , (x∈w , hv))) → PT.map (λ { (e' , r) → x , ((x∈B , x∈w) , (e' , r)) }) hv }) hx) })
其证明依次展开这两层，整个过程都留在截断之内。
cond∀∈-in : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S) → ((w : S) → ⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩ → (x e' : S) → ⟨ fst x ∈ fst B ⟩ → ⟨ fst x ∈ fst w ⟩
两道约束要求 x 同时属于基集合 B 与界项的取值 w。
→ ⟨ (e' ∷ x ∷ w ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc (suc zero))) ⟩ → ⟨ fst e' ∈ fst (Sat a) ⟩) → ⟨ (z ∷ []) ⊨ cond (∀̇∈ t a) ⟩ cond∀∈-in t a z k w hw x x∈B x∈w e' hc = k w hw x e' x∈B x∈w hc
有界全称的条件是量化三层的函数：对界项的每个取值 w，对 w 内的每个基成员 x 与每份认证为「环境 z 添加 x 后的扩展」的 e'，指派子公式在 e' 处的真值。向内映射就是这个函数被应用的样子。
cond∀∈-out : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S) → ⟨ (z ∷ []) ⊨ cond (∀̇∈ t a) ⟩ → ((w : S) → ⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩
结论量化同一个界值、基集合成员，以及经过认证的单条目扩展。
→ (x e' : S) → ⟨ fst x ∈ fst B ⟩ → ⟨ fst x ∈ fst w ⟩ → ⟨ (e' ∷ x ∷ w ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc (suc zero))) ⟩ → ⟨ fst e' ∈ fst (Sat a) ⟩) cond∀∈-out t a z h w hw x e' x∈B x∈w hc = h w hw x x∈B x∈w e' hc
向外映射是同一个函数，沿三个量词反向读出。两个方向都不出现截断：全称的验证靠供给其验证者完成，而这里验证者是一层一层供给的，为取值、为成员、也为扩展。