--- title: "常元有界性" module: FOL.Manipulation.ConstantBounding lang: zh site: "Bedrock" description: "常元有界性" stage: "一阶逻辑" reading_order: 16 canonical: https://bedrock.institute/zh/FOL.Manipulation.ConstantBounding.html html: FOL.Manipulation.ConstantBounding.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/FOL/Manipulation/ConstantBounding.lagda.md prerequisites: [Base.Prelude, FOL.Syntax, FOL.LevyHierarchy, FOL.Manipulation.ConstantMapping] routes: [fol-operations] translations: [https://bedrock.institute/en/FOL.Manipulation.ConstantBounding.md, https://bedrock.institute/ja/FOL.Manipulation.ConstantBounding.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # 常元有界性 当公式中每次出现的常元都满足一个谓词时，称该公式受此谓词约束。这些结构化证书可随谓词的蕴含而放宽，并使部分定义的常元映射恰好能对其定义域内的公式作常元改名。 本章就是那份证书。`BoundedFo P φ` 逐次出现地记录：`φ` 中出现的每个常元都满足 `P`。它按被检查公式所用的同一套分情形定义，故在模式匹配下自动拆开，任何证明都不必对「公式的常元列表」作推理。由于是纯语法，本章既不提层级也不提层，也不引入额外代价。 配套的是单调性。窄谓词的证书同时就是宽谓词的证书；这正是把针对不同层写下的证书转到公共层、以便一并使用的办法。 为什么公式要附带一份关于其常元的证书？设想一个只被部分定义的常元映射：当常元 `c` 满足某个谓词 `P` 时，它把 `c` 送到新的常元。这样的映射无法作用于任意公式，因为公式可能提到定义域之外的常元。但若我们对公式中的每次常元出现都拿到一份「该出现落在定义域内」的证明，映射就能在公式需要之处处处作用。本章要回答的问题是：这种逐出现证据应取什么形状，它又能带来什么？ ```agda {-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude module FOL.Manipulation.ConstantBounding where open import FOL.Syntax using ( Term; con; var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇ ``` 答案是一个随语法形状而定的定义。词项要么是常元，必须附带 `P` 的证明；要么是变量，不含常元，因此不施加任何条件。公式由这些构造而成，其证书也由各部分的证书组装而成。由于证书镜像了 `Term K n` 与 `Formula K n` 的构造子结构，对其作匹配就会在每次常元出现处恰好交付定义域证明。两处后续用途塑造了设计：单调性一节沿谓词间的蕴含传递证书，改名一节把证书交给部分映射；引入 Δ₀ 构造子是为了让改名后的公式保住其 Lévy 层级见证，而 Unit 类型则为一切不含常元者提供平凡证书。 ```agda ; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ ) open import FOL.LevyHierarchy using ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-⊥; δ-∀∈; δ-∃∈ ) open import FOL.Manipulation.ConstantMapping using ( mapTm; mapFo ) open import Cubical.Data.Unit using ( Unit ) ``` ## 证书 `BoundedTm P` 与 `BoundedFo P` 随语法结构而定：常元携带 `P` 的证明，变量携带平凡数据，复合公式则配有其各部分的证书。因此，模式匹配会在每次常元出现处恰好给出所需证据。 从条件最简单的词项入手。取常元上的谓词 `P` 和一个由常元 `c` 与变量构成的词项，如 `c ∈̇ var i`。证书 `BoundedTm P t` 对 `t` 递归定义：对 `con c`，证书就是 `P c` 本身，即该出现处的定义域证明；对 `var i`，证书是 `Lift Unit`，即提升到 `P c` 所在层级的单元素类型，使两种情形类型均为 `Type ℓp`。变量一无所求；其平凡证书只是把空位填上。 ```agda BoundedTm : ∀ {ℓk ℓp} {K : Type ℓk} (P : K → Type ℓp) {n} → Term K n → Type ℓp BoundedTm P (con c) = P c BoundedTm P (var i) = Lift Unit BoundedFo : ∀ {ℓk ℓp} {K : Type ℓk} (P : K → Type ℓp) {n} → Formula K n → Type ℓp BoundedFo P (t ∈̇ u) = BoundedTm P t × BoundedTm P u ``` 递归模式是统一的：凡构造子带有词项或公式参数，其证书就是各参数证书的乘积；凡构造子不提及常元，其证书就是平凡的。例如在 `(c ∈̇ d) ∧̇ ∃̇ (var 0 ≐ c)` 中常元 `c` 出现两次，证书是一个四重配对，末端是两份 `P c` 的证明：每次出现一份，位置与出现的位置对应。相反，`⊥̇` 与裸变量只携带 `Lift Unit`。所以证书跟随的是出现，而不是抽象的常元符号：同一常元出现两次就贡献两份证明。 ```agda BoundedFo P (t ≐ u) = BoundedTm P t × BoundedTm P u BoundedFo P (φ ∧̇ ψ) = BoundedFo P φ × BoundedFo P ψ BoundedFo P (φ ∨̇ ψ) = BoundedFo P φ × BoundedFo P ψ BoundedFo P (φ ⇒̇ ψ) = BoundedFo P φ × BoundedFo P ψ BoundedFo P ⊥̇ = Lift Unit ``` 量词约束的是变量，因此不触及常元，无界形式就把主体的证书原样传出。但带界量词携带一个可能提及常元的界定词项：对 `∀̇∈ t φ`，证书把 `t` 的词项证书与 `φ` 的公式证书配对，正如例式 `∃̇ (var 0 ≐ c)` 所示，其主体的证书就是 `var 0 ≐ c` 的证书。这些子句穷尽了 `Formula K n` 的构造子，而且每条子句都是从公式形状直接读出的，不是靠搜索计算出来的。 ```agda BoundedFo P (∃̇ φ) = BoundedFo P φ BoundedFo P (∀̇ φ) = BoundedFo P φ BoundedFo P (∀̇∈ t φ) = BoundedTm P t × BoundedFo P φ BoundedFo P (∃̇∈ t φ) = BoundedTm P t × BoundedFo P φ ``` ## 单调性 若 `P` 蕴含 `Q`，则每个受 `P` 约束的词项或公式也受 `Q` 约束。证明沿证书结构进行，随后可将在较小层建立的界复用于较大层。 证书只有在能于谓词之间移动时才有用。把谓词想成对允许常元的限制：沿逐点蕴含 `P⊆Q` 把 `P` 放宽为 `Q` 不会使任何证书失效，因为被 `P` 接受的每次出现仍被 `Q` 接受。对单个常元这是一次应用：`P⊆Q c` 把证明 `P c` 变成 `Q c`。`BoundedTm-mono` 对整个词项递归地扩展这一点：常元情形做那一次应用，变量情形直接通过，因为 `Lift Unit` 无论谓词如何都有元素。 ```agda module _ {ℓk ℓp ℓq} {K : Type ℓk} {P : K → Type ℓp} {Q : K → Type ℓq} (P⊆Q : (c : K) → P c → Q c) where BoundedTm-mono : ∀ {n} (t : Term K n) → BoundedTm P t → BoundedTm Q t BoundedTm-mono (con c) p = P⊆Q c p BoundedTm-mono (var i) _ = _ ``` 同一论证经证书的乘积提升到公式。以例式 `(c ∈̇ d) ∧̇ ∃̇ (var 0 ≐ c)` 为例，一份 `P` 证书是四份关于 `P` 的证明；对每个词项空位施加 `BoundedTm-mono`、对每个子公式施加递归，就把它们变成四份关于 `Q` 的证明，而公式的形状自始至终不变。 ```agda BoundedFo-mono : ∀ {n} (φ : Formula K n) → BoundedFo P φ → BoundedFo Q φ BoundedFo-mono (t ∈̇ u) (ht , hu) = BoundedTm-mono t ht , BoundedTm-mono u hu BoundedFo-mono (t ≐ u) (ht , hu) = BoundedTm-mono t ht , BoundedTm-mono u hu BoundedFo-mono (φ ∧̇ ψ) (hφ , hψ) = BoundedFo-mono φ hφ , BoundedFo-mono ψ hψ BoundedFo-mono (φ ∨̇ ψ) (hφ , hψ) = BoundedFo-mono φ hφ , BoundedFo-mono ψ hψ ``` 这一转换对任何联结词都没有特殊性：原子式与命题联结词的情形都是把证书拆成两个因子、转换因子、再重新配对，而 `⊥̇` 只需平凡证据。合取、析取、蕴涵是同一步骤的三种写法。 ```agda BoundedFo-mono (φ ⇒̇ ψ) (hφ , hψ) = BoundedFo-mono φ hφ , BoundedFo-mono ψ hψ BoundedFo-mono ⊥̇ _ = _ BoundedFo-mono (∃̇ φ) hφ = BoundedFo-mono φ hφ ``` 量词情形完成归纳。在 `∃̇` 或 `∀̇` 之下，主体被递归转换；在带界量词之下，界定词项的证书也被转换，因为该词项可能自带常元。结论是：放宽谓词就放宽了所有证书，这正是使在一层证明的界能在另一层引用的原因。 ```agda BoundedFo-mono (∀̇ φ) hφ = BoundedFo-mono φ hφ BoundedFo-mono (∀̇∈ t φ) (ht , hφ) = BoundedTm-mono t ht , BoundedFo-mono φ hφ BoundedFo-mono (∃̇∈ t φ) (ht , hφ) = BoundedTm-mono t ht , BoundedFo-mono φ hφ ``` ## 部分常元改名 部分映射能为有界公式作常元改名，因为证书在每次常元出现处提供定义域证明。将源与目标都映入同一类型后，所得公式与原式相符，并且其 Lévy 见证得以保持。 接口按使用者所需的一般性陈述：给定两个域、它们共同映入的一个世界、源上的一个谓词，以及在该谓词之下有定义的一个部分映射，另有一条等式说明该部分映射与两个投影相符。在预期的实例中，源是模型的载体，目标是某一层的成员类型，世界是层级，而那条等式表达的是「层的成员作为集合来看，仍是它原本那个集合」这一事实。 现在证书遇到了它的使用者。部分常元映射由源常元集 `K` 上的定义域谓词 `P` 与只在 `P` 上有定义的赋值 `down` 给出。要对整条公式改名，还需要目标常元集 `K'`，以及一个 `K` 与 `K'` 都映入的世界 `W`。对这些数据的数学条件是一个交换三角：对满足 `p : P c` 的每个源常元 `c`，先经 `down` 再经目标映射所落之处，与 `c` 经源映射所到之处是同一个世界元素。供给了这样的三角，由此诱导的改名在与原式都读入 `W` 之后便可验证相符。 ```agda module Relabel {ℓk ℓk' ℓv ℓp : Level} {K : Type ℓk} {K' : Type ℓk'} {W : Type ℓv} ``` 这个三角在此以参数 `down-correct` 出现：对每个 `c` 与 `p : P c`，有一条路径 `up (down c p) ≡ proj c`。这是对数据的唯一正确性义务；改名的一切其余性质都将逐出现地从它推出。注意 `down` 需要证明 `p` 作为参数：证书正是使部分映射可施用的东西，恰在公式提及常元之处供给其定义域条件。 ```agda (proj : K → W) (up : K' → W) (P : K → Type ℓp) (down : (c : K) → P c → K') (down-correct : (c : K) (p : P c) → up (down c p) ≡ proj c) ``` 对词项改名只需把证书穿起来。`liftTm` 接受 `t` 连同 `h : BoundedTm P t`；在常元结点对 `h` 作匹配，恰好交出 `down c` 所需的证明 `p : P c`，于是结点变成 `con (down c p)`。在变量处，`h` 是平凡的，结点原样通过。部分映射变成了全映射，但只对出示定义域证明的词项如此。 ```agda where liftTm : ∀ {n} (t : Term K n) → BoundedTm P t → Term K' n liftTm (con c) p = con (down c p) liftTm (var i) _ = var i liftFo : ∀ {n} (φ : Formula K n) → BoundedFo P φ → Formula K' n ``` 对公式，`liftFo` 在词项空位施加 `liftTm`，其余处递归。在前面的例子中，`c` 的两次出现被替换为 `down c` 在其两份证明处的值，`d` 同理，而约束变元结构不受影响：改名只改写常元，从不触及 de Bruijn 指标，因此自由变元个数仍为 `n`。 ```agda liftFo (t ∈̇ u) (ht , hu) = liftTm t ht ∈̇ liftTm u hu liftFo (t ≐ u) (ht , hu) = liftTm t ht ≐ liftTm u hu liftFo (φ ∧̇ ψ) (hφ , hψ) = liftFo φ hφ ∧̇ liftFo ψ hψ liftFo (φ ∨̇ ψ) (hφ , hψ) = liftFo φ hφ ∨̇ liftFo ψ hψ liftFo (φ ⇒̇ ψ) (hφ , hψ) = liftFo φ hφ ⇒̇ liftFo ψ hψ ``` 带界量词重复同样的两件套形状：对界定词项改名并对主体递归；`⊥̇` 与无界量词则没有可改名的常元。于是对任何携带证书的公式，`liftFo φ h` 总有定义，下一节的相符定理将精确说明它在何种意义上与 `φ` 是同一条公式。 ```agda liftFo ⊥̇ _ = ⊥̇ liftFo (∃̇ φ) hφ = ∃̇ liftFo φ hφ liftFo (∀̇ φ) hφ = ∀̇ liftFo φ hφ liftFo (∀̇∈ t φ) (ht , hφ) = ∀̇∈ (liftTm t ht) (liftFo φ hφ) liftFo (∃̇∈ t φ) (ht , hφ) = ∃̇∈ (liftTm t ht) (liftFo φ hφ) ``` 正确性说明这次常元改名没有改变任何要紧的东西：沿 `up` 把结果推进共同世界 `W`，与沿 `proj` 把原式推进去，得到的是同一条公式。那正是绝对性论证中两条途径会合时所需的等式，而它逐次出现地成立，理由正是接口 `down-correct` 所索取的那一条。Δ₀ 见证同样得以保留：该证书记录的只是量词结构，在常元改名之下原样转移。 两件事实为三角的故事收尾。其一，把提升后的词项沿 `up` 改名到共同常元域 `W`，与把原词项沿 `proj` 改名所得的词项相同；其二，改名保持 Δ₀ 证书，因为它改动的是常元而非量词结构。基例是词项。对常元 `con c`，证书提供 `p : P c`，所需路径就是把三角的边 `down-correct c p` 经 `cong con` 放置。对 `var i`，两边都计算为对同一变量的 `mapTm _ (var i)`，故路径是 `refl`。 ```agda liftTm-correct : ∀ {n} (t : Term K n) (h : BoundedTm P t) → mapTm up (liftTm t h) ≡ mapTm proj t liftTm-correct (con c) p = cong con (down-correct c p) liftTm-correct (var i) _ = refl liftFo-correct : ∀ {n} (φ : Formula K n) (h : BoundedFo P φ) ``` 公式层面的陈述比较作用于 `φ` 的两个复合 `mapFo up ∘ liftFo` 与 `mapFo proj`。像 `t ∈̇ u` 这样的原子式已经显出机制：目标拆成对 `t` 与 `u` 的两个词项目标，由基例供给，`cong₂ _∈̇_` 把它们放到属于符号之下。 ```agda → mapFo up (liftFo φ h) ≡ mapFo proj φ liftFo-correct (t ∈̇ u) (ht , hu) = cong₂ _∈̇_ (liftTm-correct t ht) (liftTm-correct u hu) liftFo-correct (t ≐ u) (ht , hu) = cong₂ _≐_ (liftTm-correct t ht) (liftTm-correct u hu) ``` 复合公式没有新内容：每个二元联结词情形都对符号施加 `cong₂`，并配上来自子公式的两条递归路径。归纳只是跟随证书自身的配对结构，这正是当初把证书设计成镜像语法的原因。 ```agda liftFo-correct (φ ∧̇ ψ) (hφ , hψ) = cong₂ _∧̇_ (liftFo-correct φ hφ) (liftFo-correct ψ hψ) liftFo-correct (φ ∨̇ ψ) (hφ , hψ) = cong₂ _∨̇_ (liftFo-correct φ hφ) (liftFo-correct ψ hψ) liftFo-correct (φ ⇒̇ ψ) (hφ , hψ) = ``` 不含常元的形式更容易：`⊥̇` 在两条途径下都映到自身，给出 `refl`；无界量词情形各用 `cong` 把唯一一条递归路径包在量词符号之下，因为前缀不引入常元。 ```agda cong₂ _⇒̇_ (liftFo-correct φ hφ) (liftFo-correct ψ hψ) liftFo-correct ⊥̇ _ = refl liftFo-correct (∃̇ φ) hφ = cong ∃̇_ (liftFo-correct φ hφ) liftFo-correct (∀̇ φ) hφ = cong ∀̇_ (liftFo-correct φ hφ) liftFo-correct (∀̇∈ t φ) (ht , hφ) = ``` 带界量词把两类情形合在一起：其词项路径与主体路径经 `cong₂` 在量词构造子之下合并，归纳至此完成。声明 `Δ₀-liftFo` 转向第二件被允诺的事实。其陈述是一次转移：给定 `φ` 的有界证书 `h` 与 `φ` 的一个 Δ₀ 见证，它返回 `liftFo φ h` 的一个 Δ₀ 见证。基例是原子见证 `δ-∈`，它不携带数据，原样保留。 ```agda cong₂ ∀̇∈ (liftTm-correct t ht) (liftFo-correct φ hφ) liftFo-correct (∃̇∈ t φ) (ht , hφ) = cong₂ ∃̇∈ (liftTm-correct t ht) (liftFo-correct φ hφ) Δ₀-liftFo : ∀ {n} {φ : Formula K n} (h : BoundedFo P φ) → Δ₀ φ → Δ₀ (liftFo φ h) Δ₀-liftFo (ht , hu) δ-∈ = δ-∈ ``` 递归沿 Δ₀ 见证而非公式进行；证书被拆开只是为了取到与每个子见证配对的子证书。联结词情形用转移后的子见证重建其构造子，假则直接返回 `δ-⊥`。 ```agda Δ₀-liftFo (ht , hu) δ-≐ = δ-≐ Δ₀-liftFo (hφ , hψ) (δ-∧ c d) = δ-∧ (Δ₀-liftFo hφ c) (Δ₀-liftFo hψ d) Δ₀-liftFo (hφ , hψ) (δ-∨ c d) = δ-∨ (Δ₀-liftFo hφ c) (Δ₀-liftFo hψ d) Δ₀-liftFo (hφ , hψ) (δ-⇒ c d) = δ-⇒ (Δ₀-liftFo hφ c) (Δ₀-liftFo hψ d) Δ₀-liftFo _ δ-⊥ = δ-⊥ ``` 带界量词见证完成递归：各自把一个转移后的子见证包入 `δ-∀∈` 或 `δ-∃∈`。由于每个 Δ₀ 构造子都已处理，转移是全的，公式的 Δ₀ 身份不因常元改名而改变。 ```agda Δ₀-liftFo (ht , hφ) (δ-∀∈ c) = δ-∀∈ (Δ₀-liftFo hφ c) Δ₀-liftFo (ht , hφ) (δ-∃∈ c) = δ-∃∈ (Δ₀-liftFo hφ c) ``` ## 小结 常元有界语法打包了部分常元映射所需的证据。单调性沿谓词间的逐点蕴涵传递这些证据。随后，`liftTm` 与 `liftFo`、它们的相符性引理以及 `Δ₀-liftFo` 完成带证书的常元改名，并保持这里陈述的语法性质。