常元有界性

可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。

阅读指南 · 依赖地图

当公式中每次出现的常元都满足一个谓词时，称该公式受此谓词约束。这些结构化证书可随谓词的蕴含而放宽，并使部分定义的常元映射恰好能对其定义域内的公式作常元改名。

本章就是那份证书。BoundedFo P φ 逐次出现地记录：φ 中出现的每个常元都满足 P。它按被检查公式所用的同一套分情形定义，故在模式匹配下自动拆开，任何证明都不必对「公式的常元列表」作推理。由于是纯语法，本章既不提层级也不提层，也不引入额外代价。

配套的是单调性。窄谓词的证书同时就是宽谓词的证书；这正是把针对不同层写下的证书转到公共层、以便一并使用的办法。

为什么公式要附带一份关于其常元的证书？设想一个只被部分定义的常元映射：当常元 c 满足某个谓词 P 时，它把 c 送到新的常元。这样的映射无法作用于任意公式，因为公式可能提到定义域之外的常元。但若我们对公式中的每次常元出现都拿到一份「该出现落在定义域内」的证明，映射就能在公式需要之处处处作用。本章要回答的问题是：这种逐出现证据应取什么形状，它又能带来什么？

{-# 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 类型则为一切不含常元者提供平凡证书。

        ; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
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。变量一无所求；其平凡证书只是把空位填上。

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。所以证书跟随的是出现，而不是抽象的常元符号：同一常元出现两次就贡献两份证明。

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 的构造子，而且每条子句都是从公式形状直接读出的，不是靠搜索计算出来的。

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 无论谓词如何都有元素。

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 的证明，而公式的形状自始至终不变。

  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ψ

这一转换对任何联结词都没有特殊性：原子式与命题联结词的情形都是把证书拆成两个因子、转换因子、再重新配对，而 ⊥̇ 只需平凡证据。合取、析取、蕴涵是同一步骤的三种写法。

  BoundedFo-mono (φ ⇒̇ ψ)  (hφ , hψ) = BoundedFo-mono φ hφ , BoundedFo-mono ψ hψ
  BoundedFo-mono ⊥̇        _         = _
  BoundedFo-mono (∃̇ φ)    hφ        = BoundedFo-mono φ hφ

量词情形完成归纳。在 ∃̇ 或 ∀̇ 之下，主体被递归转换；在带界量词之下，界定词项的证书也被转换，因为该词项可能自带常元。结论是：放宽谓词就放宽了所有证书，这正是使在一层证明的界能在另一层引用的原因。

  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 之后便可验证相符。

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 作为参数：证书正是使部分映射可施用的东西，恰在公式提及常元之处供给其定义域条件。

  (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 是平凡的，结点原样通过。部分映射变成了全映射，但只对出示定义域证明的词项如此。

  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。

  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 总有定义，下一节的相符定理将精确说明它在何种意义上与 φ 是同一条公式。

  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。

  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₂ _∈̇_ 把它们放到属于符号之下。

                 → 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₂，并配上来自子公式的两条递归路径。归纳只是跟随证书自身的配对结构，这正是当初把证书设计成镜像语法的原因。

  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 把唯一一条递归路径包在量词符号之下，因为前缀不引入常元。

    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 的一个 Δ₀ 见证。基例是原子见证 δ-∈，它不携带数据，原样保留。

    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) δ-∈       = δ-∈

递归沿 Δ₀ 见证而非公式进行；证书被拆开只是为了取到与每个子见证配对的子证书。联结词情形用转移后的子见证重建其构造子，假则直接返回 δ-⊥。

  Δ₀-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 _         δ-⊥       = δ-⊥

带界量词见证完成递归：各自把一个转移后的子见证包入 δ-∀∈ 或 δ-∃∈。由于每个 Δ₀ 构造子都已处理，转移是全的，公式的 Δ₀ 身份不因常元改名而改变。

  Δ₀-liftFo (ht , hφ) (δ-∀∈ c)  = δ-∀∈ (Δ₀-liftFo hφ c)
  Δ₀-liftFo (ht , hφ) (δ-∃∈ c)  = δ-∃∈ (Δ₀-liftFo hφ c)

小结

常元有界语法打包了部分常元映射所需的证据。单调性沿谓词间的逐点蕴涵传递这些证据。随后，liftTm 与 liftFo、它们的相符性引理以及 Δ₀-liftFo 完成带证书的常元改名，并保持这里陈述的语法性质。