---
title: "单点集与有序对的公式"
module: L.Coding.PairFormulas
lang: zh
site: "Bedrock"
description: "单点集与有序对的公式"
stage: "内部编码：表达式与定义域"
reading_order: 40
canonical: https://bedrock.institute/zh/L.Coding.PairFormulas.html
html: L.Coding.PairFormulas.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/PairFormulas.lagda.md
prerequisites: [Base.Prelude, FOL.Syntax, FOL.LevyHierarchy, FOL.Semantics, V.Hierarchy, V.Coding]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.PairFormulas.md, https://bedrock.institute/ja/L.Coding.PairFormulas.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 单点集与有序对的公式

本章的目标是让对象语言识别出某个被指派的集合恰是另外两个集合的 Kuratowski 有序对，顺带识别出 Kuratowski 对由之构成的单点集与无序对。一阶公式只能谈论隶属与相等，故识别必须是外延的：识别 `pr U W`，就是仅凭隶属说出它恰有哪些成员。本章构造三条有界公式：`sglAt` 说「这个集合是那个集合的单点集」，`pairAt` 说「这是那两个集合的无序对」，`prAt` 把这些组合成「这是那两个集合的 Kuratowski 对」。

结尾的充分性定理是一条精确的等同。对任意赋值，`prAt q u v` 的满足关系是一条真值路径，通向「`q` 处的值等于 `pr` 作用在 `u`、`v` 处之值上的结果」这一命题。这里不断言任何更弱的陈述，例如单向蕴含。

由于每条公式的量词都以某个被指派的集合为界，其自由变元位置取作参数给出的 de Bruijn 下标，同一条公式在任何嵌套深度都能使用。每条子句都是原子或有界量词，故每条读式都是 Lévy 层级中的 Δ₀。

外部目标有明确的成员形状：`pr U W = ⁅ ⁅ U ⁆s , ⁅ U , W ⁆ ⁆`。其外层集合是一个无序对，第一个成员是 `U` 的单点集，第二个成员是 `U` 与 `W` 的无序对。因此，识别这个有序对可归结为三项条件：两个指定成员都出现，并且每个成员都是二者之一。最后一项采用命题截断，正好对应无序对隶属的分类；它记录这项选择，却不指定是哪一侧。

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

open import Base.Prelude

module L.Coding.PairFormulas {ℓ : Level} where

open import FOL.Syntax
```

表达这些描述的工具是一阶语言的有界片段。其原子 `_∈̇_` 与 `_≐_` 及联结词 `_∧̇_` 与 `_∨̇_` 陈述各位置上被指派集合之间的隶属与相等；其量词 `∀̇∈` 与 `∃̇∈` 总以某个被指派的集合为界。仅由这些构造的公式组成 Lévy 层级中的有界类 `Δ₀`，并由 `checkΔ₀` 作语法检查。

识别的对象是 Kuratowski 编码 `pr`，定义为 `pr U W = ⁅ ⁅ U ⁆s , ⁅ U , W ⁆ ⁆`：有序对被呈现为两个集合的无序对，即 `U` 的单点集与 `U` 和 `W` 的对。于是识别问题归结为：用有界公式说一个集合有一个成员是 `U` 的单点集、有一个成员是 `U` 与 `W` 的无序对、且没有别的成员。单点集与无序对的隶属各有自己的分类，而外延性将把完备的隶属条件转换为集合间的等式。

```agda
  using ( var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; ∀̇∈; ∃̇∈ )
open import FOL.LevyHierarchy using ( Δ₀; checkΔ₀ )
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV )
open import V.Coding {ℓ} using ( pr )
```

单点集与无序对的隶属各有两种等价形式：层级隶属 `⟨ y ∈ b ⟩`，以及相应构造所使用的小隶属分类；`∈∈ₛ` 在两者之间转换。对单点集，分类给出路径 `y ≡ u`；对无序对，分类给出截断的两种可能 `∥ (y ≡ u) ⊎ (y ≡ v) ∥₁`。分别证明这些隶属描述的两个方向后，`⇔toPath` 把每一对隶属命题的等价转成外延性所需的路径。

```agda
open import Cubical.Data.Unit using ( tt )
import Cubical.Data.Sum as Sum
open Sum using ( _⊎_; inl; inr )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁ )
```

语义以层级 `ℓ-suc ℓ` 上的 `hProp` 为真值。公式不取值为一个裸的布尔值：其值是一个命题，而一个赋值下公式的满足关系本身就是一个命题，而非一个判定。解读复合公式时，合取与析取直接作用于这些 `hProp` 真值。这一命题化设定对目标至关重要：它使一条有界公式的满足关系能够逐路径地等同于一个外部条件，例如某集合与其编码对相等。

```agda
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈∈ₛ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
```

在此语义中，常元解释被固定为 `V ℓ` 上的恒等：语言中的一个常元就是一个集合，指称它自身。于是 `⟦ var k ⟧ γ` 是环境 `γ` 分派给位置 `k` 的值，公式从而可以直接谈论被指派的集合。

```agda
  using ( ⁅_,_⁆; pairing-ax; ⁅_⁆s; SingletonPackage; module InfinitySet )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( SetPackage )  -- lint-agda: keep (used qualified: SetPackage.classification)
open InfinitySet using ( #_ )
```

这正是下面充分性陈述有意义的原因：读式 `prAt` 在位置 `q`、`u`、`v` 上的满足关系将作为真值，与 `⟦ var q ⟧ γ` 和 `pr (⟦ var u ⟧ γ) (⟦ var v ⟧ γ)` 的相等相比较。

```agda
module Sem = FOL.Semantics 𝒮ᵥ
open Sem using ( _^_ )
open Sem.At (V ℓ) id using ( _⊨_; ⟦_⟧ )
```

## 单点集与无序对的特征刻画

唯一成员为 `u` 的集合就是 `u` 的单点集，而成员恰为 `u` 与 `v` 的集合就是它们的无序对。这些正是对象语言读式将要表达的外部含义，故在元层于此一次性证明。两条特征刻画依赖同一个手法：若两个集合允许相同的成员，外延性 `extensionalV` 便把逐点的隶属等价变成集合间的路径。

两个方向的强度不同。`⁅ u ⁆s` 的成员等于 `u` 是一条没有外层截断的路径；`⁅ u , v ⁆` 的成员是 `u` 或 `v` 则仅仅是如此，是一个命题截断的析取。证明严格保持了这一区分。

对单点集的隶属被 `SingletonPackage` 的分类完全刻画：`y` 属于 `⁅ u ⁆s`，恰好当 `y` 等于 `u`。桥 `∈∈ₛ` 在层级的原生隶属与这一小隶属之间转换，于是 `∈sgl-elim` 把桥的前半段与分类串联起来，从仅仅一条隶属证明中提取出直接的路径 `y ≡ u`；`∈sgl-intro` 把同样的两步反向执行。这里没有任何截断：相等路径可直接使用；由于 `V ℓ` 是 h-集合，这仍是命题。

```agda
∈sgl-elim : {u y : V ℓ} → ⟨ y ∈ ⁅ u ⁆s ⟩ → y ≡ u
∈sgl-elim {u} {y} h =
    SetPackage.classification (SingletonPackage u) y .fst (∈∈ₛ {a = y} {b = ⁅ u ⁆s} .fst h)

∈sgl-intro : {u y : V ℓ} → y ≡ u → ⟨ y ∈ ⁅ u ⁆s ⟩
∈sgl-intro {u} {y} e = ∈∈ₛ {a = y} {b = ⁅ u ⁆s} .snd
```

对无序对，分类 `pairing-ax` 用析取刻画隶属：成员等于 `u` 或等于 `v`。截断正是在此出现。`∈pair-elim` 把隶属证明转换为仅仅成立的析取 `∥ (y ≡ u) ⊎ (y ≡ v) ∥₁`，因为底层的分类返回的是命题截断的两种可能，而不允许把它消去到未截断的和类型。反过来，`∈pair-introL` 与 `∈pair-introR` 各取一侧的直接给出的路径，把它封为「仅仅这一侧或那一侧」，从而得到隶属。

```agda
    (SetPackage.classification (SingletonPackage u) y .snd e)

∈pair-elim : {u v y : V ℓ} → ⟨ y ∈ ⁅ u , v ⁆ ⟩ → ∥ (y ≡ u) ⊎ (y ≡ v) ∥₁
∈pair-elim {u} {v} {y} h = pairing-ax u v y .fst (∈∈ₛ {a = y} {b = ⁅ u , v ⁆} .fst h)

∈pair-introL : {u v y : V ℓ} → y ≡ u → ⟨ y ∈ ⁅ u , v ⁆ ⟩
∈pair-introL {u} {v} {y} e = ∈∈ₛ {a = y} {b = ⁅ u , v ⁆} .snd
```

第二条引入与第一条对称。进入与离开这两个构造的隶属都齐备后，外部特征刻画便可陈述。`sgl-char` 说：若 `u` 属于 `x` 且 `x` 的每个成员都等于 `u`，则 `x` 是 `u` 的单点集。`pair-char` 对两个分量说类似的话，只是「每个成员」条款此刻是仅仅成立的析取。两条结论都是集合间的路径，而且之后都将恰好供给读式 `prAt` 所表达的那些子句。

```agda
    (pairing-ax u v y .snd ∣ inl e ∣₁)

∈pair-introR : {u v y : V ℓ} → y ≡ v → ⟨ y ∈ ⁅ u , v ⁆ ⟩
∈pair-introR {u} {v} {y} e = ∈∈ₛ {a = y} {b = ⁅ u , v ⁆} .snd
    (pairing-ax u v y .snd ∣ inr e ∣₁)

sgl-char : (x u : V ℓ) → ⟨ u ∈ x ⟩ → ((y : V ℓ) → ⟨ y ∈ x ⟩ → y ≡ u) → x ≡ ⁅ u ⁆s
```

要从两条隶属假设证明 `x ≡ ⁅ u ⁆s`，需逐点使用外延性：对每个 `y`，命题 `⟨ y ∈ x ⟩` 必须经一条路径与 `⟨ y ∈ ⁅ u ⁆s ⟩` 相连，而 `⇔toPath` 恰好从当且仅当构造出这样的路径。前进方向使用「`x` 的所有成员都等于 `u`」这一假设，再重新引入对单点集的隶属；这就是 `sub₁`。

```agda
sgl-char x u hu hall = extensionalV (λ y → ⇔toPath (sub₁ y) (sub₂ y))
  where
  sub₁ : (y : V ℓ) → ⟨ y ∈ x ⟩ → ⟨ y ∈ ⁅ u ⁆s ⟩
  sub₁ y hy = ∈sgl-intro (hall y hy)
  sub₂ : (y : V ℓ) → ⟨ y ∈ ⁅ u ⁆s ⟩ → ⟨ y ∈ x ⟩
```

反向的 `sub₂` 从对单点集的隶属出发，须产出对 `x` 的隶属。消去给出路径 `y ≡ u`，再沿其逆把隶属传输过去：若 `u` 属于 `x` 而 `y` 与 `u` 相差一条路径，则 `y` 也属于 `x`。这种「沿路径传输」的模式是直接比较各构造的标准替代品，在本章其余每个证明中都会重现。两个方向就位后，`⇔toPath` 组装出逐点等价，`extensionalV` 返回路径 `x ≡ ⁅ u ⁆s`。

```agda
  sub₂ y hy = subst (λ z → ⟨ z ∈ x ⟩) (sym (∈sgl-elim hy)) hu

pair-char : (x u v : V ℓ) → ⟨ u ∈ x ⟩ → ⟨ v ∈ x ⟩
          → ((y : V ℓ) → ⟨ y ∈ x ⟩ → ∥ (y ≡ u) ⊎ (y ≡ v) ∥₁)
          → x ≡ ⁅ u , v ⁆
pair-char x u v hu hv hall = extensionalV (λ y → ⇔toPath (sub₁ y) (sub₂ y))
```

`pair-char` 的证明遵循同一计划，但有一个新特点：「每个成员」假设是截断的，故前进方向 `sub₁` 不能对 `y` 在哪一侧做模式匹配。它改为用 `PT.rec` 把截断消去到确为命题值的隶属命题 `⟨ y ∈ ⁅ u , v ⁆ ⟩` 中，再在和类型的两侧上分派：等于 `u` 的成员从左边进入那个对，等于 `v` 的成员从右边进入。这是使用仅仅成立的析取事实的正当方式。

```agda
  where
  sub₁ : (y : V ℓ) → ⟨ y ∈ x ⟩ → ⟨ y ∈ ⁅ u , v ⁆ ⟩
  sub₁ y hy = PT.rec ((y ∈ ⁅ u , v ⁆) .snd)
    (Sum.rec (∈pair-introL {u = u} {v = v}) (∈pair-introR {u = u} {v = v})) (hall y hy)
  sub₂ : (y : V ℓ) → ⟨ y ∈ ⁅ u , v ⁆ ⟩ → ⟨ y ∈ x ⟩
```

反向的 `sub₂` 与之镜像：从对 `⁅ u , v ⁆` 的隶属经 `∈pair-elim` 得到截断析取，把它消去到隶属命题 `⟨ y ∈ x ⟩` 中，并在每个分支里沿还原出的路径把相应的假设 `hu` 或 `hv` 反向传输。于是 `sub₁` 与 `sub₂` 都只凭对构造的分类就制造出对 `x` 的隶属，`extensionalV` 再把逐点的结果升级为 `x ≡ ⁅ u , v ⁆`。

```agda
  sub₂ y hy = PT.rec ((y ∈ x) .snd)
    (Sum.rec (λ e → subst (λ z → ⟨ z ∈ x ⟩) (sym e) hu)
             (λ e → subst (λ z → ⟨ z ∈ x ⟩) (sym e) hv)) (∈pair-elim hy)
```

## 元层的 Kuratowski 对

读式 `prAt` 将对一个集合 `Q` 说：它有一个成员是 `U` 的单点集，有一个成员是 `U` 与 `W` 的无序对，且每个成员都是这两者之一。本节证明恰好这三条条件迫使 `Q` 等于 Kuratowski 对 `pr U W = ⁅ ⁅ U ⁆s , ⁅ U , W ⁆ ⁆`，并证明其逆。下面的两个辅助谓词逐条记录这些条件，其形状恰好是 bounded 公式的满足关系将要展开成的形状；于是充分性一节的语义引理可以直接把假设交给这里证明的元层引理，而不必再证一遍。

第一个谓词 `SglOf U w` 用纯粹的隶属语言说 `w` 是 `U` 的单点集：`U` 属于 `w`，且任何属于 `w` 的 `z` 都实实在在地等于 `U`。第二个谓词 `PairOf U W w` 说 `w` 是无序对：`U` 与 `W` 都属于 `w`，且每个成员仅仅是二者之一，即一个命题截断的析取。二者都居于层级 `ℓ-suc ℓ`，因为对所有 `V ℓ` 中的集合量化要花掉一个层级，与语义取真值的层级相同。

```agda
private
  SglOf : V ℓ → V ℓ → Type (ℓ-suc ℓ)
  SglOf U w = ⟨ U ∈ w ⟩ × ((z : V ℓ) → ⟨ z ∈ w ⟩ → z ≡ U)

  PairOf : V ℓ → V ℓ → V ℓ → Type (ℓ-suc ℓ)
  PairOf U W w =
```

这些包装经由上一节的特征刻画与等式相连。若 `w` 携带 `SglOf U`，其两个分量恰是 `sgl-char` 的假设，后者返回路径 `w ≡ ⁅ U ⁆s`；类似地，`pair-char` 把 `PairOf` 包装变成 `w ≡ ⁅ U , W ⁆`。于是包装就是与相应构造相等的证书，而且取得它无需检查 `w` 是如何构造的。

```agda
    ⟨ U ∈ w ⟩ × (⟨ W ∈ w ⟩ × ((z : V ℓ) → ⟨ z ∈ w ⟩ → ∥ (z ≡ U) ⊎ (z ≡ W) ∥₁))

  sglOf→≡ : {U w : V ℓ} → SglOf U w → w ≡ ⁅ U ⁆s
  sglOf→≡ {U} {w} (hu , hall) = sgl-char w U hu hall

  pairOf→≡ : {U W w : V ℓ} → PairOf U W w → w ≡ ⁅ U , W ⁆
  pairOf→≡ {U} {W} {w} (hu , hv , hall) = pair-char w U W hu hv hall
```

反向的数据也存在：这些构造本身就携带自己的包装。对 `⁅ U ⁆s` 而言，`U` 的隶属由在自反路径上使用 `∈sgl-intro` 得到，而每个成员等于 `U` 由 `∈sgl-elim` 得到；无序对用两条引入与 `∈pair-elim` 以同样方式包装。最后，由于包装是关于集合 `w` 的取命题值的类型，它可以沿集合间的路径传输：从 `w ≡ ⁅ U ⁆s` 出发，把 `⁅ U ⁆s` 的包装沿路径反向传输，便得到 `SglOf U w`。

```agda
  sglOf⁅⁆ : (U : V ℓ) → SglOf U ⁅ U ⁆s
  sglOf⁅⁆ U = ∈sgl-intro refl , (λ z z∈ → ∈sgl-elim z∈)

  pairOf⁅⁆ : (U W : V ℓ) → PairOf U W ⁅ U , W ⁆
  pairOf⁅⁆ U W = ∈pair-introL refl , ∈pair-introR refl , (λ z z∈ → ∈pair-elim z∈)

  sglOf-subst : {U w : V ℓ} → w ≡ ⁅ U ⁆s → SglOf U w
```

包装就位后，元层特征刻画便可陈述。`prChar-fwd` 取三条假设，得出路径 `Q ≡ pr U W`。前两条是截断的存在陈述：仅仅存在 `Q` 的某个成员 `w` 携带 `SglOf U`，仅仅存在 `Q` 的某个成员 `w` 携带 `PairOf U W`。第三条是全称条款：`Q` 的每个成员 `y` 仅仅是 `U` 的单点集或 `U` 与 `W` 的对。注意 `pr U W` 的外层集合是一个无序对，其两个成员编码了有序的分量；下面将通过 `pair-char` 证明 `Q` 等于这个外层对。

```agda
  sglOf-subst {U} e = subst (SglOf U) (sym e) (sglOf⁅⁆ U)

  pairOf-subst : {U W w : V ℓ} → w ≡ ⁅ U , W ⁆ → PairOf U W w
  pairOf-subst {U} {W} e = subst (PairOf U W) (sym e) (pairOf⁅⁆ U W)

prChar-fwd : (Q U W : V ℓ)
  → ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × SglOf U w) ∥₁
```

前两条假设各自仅仅给出 `Q` 的一个成员以及证明该成员等于相应构造的包装。截断被消去到隶属命题 `⟨ ⁅ U ⁆s ∈ Q ⟩` 或 `⟨ ⁅ U , W ⁆ ∈ Q ⟩` 中，二者都取命题值，故无需让见证的选取保持一致。在每个分支内，包装被转换为路径 `w ≡ ⁅ U ⁆s` 或 `w ≡ ⁅ U , W ⁆`，并把 `w` 的隶属沿它传输，得到该构造对 `Q` 的隶属。这正是 `pair-char` 所需的前两个参数，只是 `u` 与 `v` 的位置换成了 `⁅ U ⁆s` 与 `⁅ U , W ⁆`。

```agda
  → ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × PairOf U W w) ∥₁
  → ((y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ SglOf U y ⊎ PairOf U W y ∥₁)
  → Q ≡ pr U W
prChar-fwd Q U W h₁ h₂ h₃ = pair-char Q ⁅ U ⁆s ⁅ U , W ⁆
  (PT.rec ((⁅ U ⁆s ∈ Q) .snd)
```

全称条款根本不需要消去：对 `Q` 的每个成员 `y`，把包装的截断析取经转换 `sglOf→≡` 与 `pairOf→≡` 映过去，得到「`y` 仅仅等于 `⁅ U ⁆s` 或 `⁅ U , W ⁆`」的截断陈述。这便是 `pair-char` 的第三个参数。其结论即 `Q ≡ ⁅ ⁅ U ⁆s , ⁅ U , W ⁆ ⁆`，按定义就是 `Q ≡ pr U W`。逆向的 `prChar-bwd` 则只需为 Kuratowski 对本身展示这三条假设。

```agda
    (λ { (w , hw , h) → subst (λ z → ⟨ z ∈ Q ⟩) (sglOf→≡ h) hw }) h₁)
  (PT.rec ((⁅ U , W ⁆ ∈ Q) .snd)
    (λ { (w , hw , h) → subst (λ z → ⟨ z ∈ Q ⟩) (pairOf→≡ h) hw }) h₂)
  (λ y hy → PT.map (Sum.map sglOf→≡ pairOf→≡) (h₃ y hy))

prChar-bwd : (Q U W : V ℓ) → Q ≡ pr U W
```

给定路径 `Q ≡ pr U W` 后，三条假设依次产出。辅助工具 `inQ` 沿路径的逆把对 `pr U W` 的隶属传输为对 `Q` 的隶属，三条分量都将用到它。

```agda
  → (∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × SglOf U w) ∥₁)
  × ((∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × PairOf U W w) ∥₁)
  × ((y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ SglOf U y ⊎ PairOf U W y ∥₁))
prChar-bwd Q U W e = h₁ , h₂ , h₃
  where
```

第一条存在陈述由 `⁅ U ⁆s` 自己作见证：它属于 `pr U W`，因为外层对含有其第一个分量，即在自反路径上的 `∈pair-introL` 的实例；经 `inQ` 传输后这条隶属在 `Q` 中成立；而它携带 `SglOf U` 则由包装 `sglOf⁅⁆` 给出。第二条同样，换用 `⁅ U , W ⁆`、`∈pair-introR` 与 `pairOf⁅⁆`。二者按其类型的要求都以截断封口；由于目标只是存在陈述，所选的见证便已足够。

```agda
  inQ : {z : V ℓ} → ⟨ z ∈ pr U W ⟩ → ⟨ z ∈ Q ⟩
  inQ {z} h = subst (λ w → ⟨ z ∈ w ⟩) (sym e) h
  h₁ : ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × SglOf U w) ∥₁
  h₁ = ∣ ⁅ U ⁆s , (inQ (∈pair-introL refl) , sglOf⁅⁆ U) ∣₁
  h₂ : ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × PairOf U W w) ∥₁
```

全称条款归结为对构造的分类。对 `Q` 的成员 `y`，沿路径传输给出 `y` 对 `pr U W` 的隶属，`∈pair-elim` 把它转换为截断析取：`y ≡ ⁅ U ⁆s` 或 `y ≡ ⁅ U , W ⁆`。每一侧经传输引理 `sglOf-subst` 与 `pairOf-subst` 升级为相应的包装，于是该映射把路径的析取变为包装的析取，而自始至终不展开任何一个构造。

```agda
  h₂ = ∣ ⁅ U , W ⁆ , (inQ (∈pair-introR refl) , pairOf⁅⁆ U W) ∣₁
  h₃ : (y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ SglOf U y ⊎ PairOf U W y ∥₁
  h₃ y y∈Q = PT.map (Sum.rec (λ q → inl (sglOf-subst q)) (λ q → inr (pairOf-subst q)))
    (∈pair-elim (subst (λ w → ⟨ y ∈ w ⟩) e y∈Q))
```

## 对象语言中的读式

现在把外部的特征刻画写成对象语言的公式。每条读式把它所谈论的 de Bruijn 位置取作参数，故同一条定义在任何嵌套深度都能使用。有界量化的记账是标准做法：有界量词在位置零绑定一个新变元，并把原有位置向外推一步，故在约束下提到的位置以其后继出现。由于每条子句都是原子、合取或析取、或以环境中变元为界的量词，每条读式都是 Δ₀，且其界定集合直接从形状可见。

单点集读式 `sglAt k i` 对位置 `k` 与 `i` 上指派的集合说：`i` 处的是 `k` 处的单点集。第一个合取支是原子 `var i ∈̇ var k`；第二个合取支以 `var k` 的成员为界量化，并在其内把位置零上新绑定的变元与 `var (suc i)` 比较，后者是 `i` 在约束下经一步移位后的位置。一个集合满足这条读式，恰好当它有一个等于 `k` 值的成员且没有别的成员，即 `SglOf` 的内容。

```agda
sglAt : ∀ {n} → Fin n → Fin n → Formula (V ℓ) n
sglAt k i = (var i ∈̇ var k) ∧̇ (∀̇∈ (var k) (var zero ≐ var (suc i)))
```

无序对读式 `pairAt k i j` 添加第二个分量，并把全称条款弱化为析取。在有界量词之下，位置零上的新变元与两个移位后的参数位置 `var (suc i)` 与 `var (suc j)` 都作比较。从外部读，一个集合满足它，当 `i` 与 `j` 处的值都属于它且每个成员仅仅等于二者之一，这恰是包装 `PairOf`。注意 `_∧̇_` 与 `_∨̇_` 的结合性声明只控制这些表达式如何解析；这里不断言任何联结词的结合律。

```agda
pairAt : ∀ {n} → Fin n → Fin n → Fin n → Formula (V ℓ) n
pairAt k i j = (var i ∈̇ var k) ∧̇ ((var j ∈̇ var k)
            ∧̇ (∀̇∈ (var k) ((var zero ≐ var (suc i)) ∨̇ (var zero ≐ var (suc j)))))
```

组装好的对读式把两条较小的读式与元层特征刻画的三条子句合在一起：某个成员是那个单点集，某个成员是那个对，且每个成员二者居其一。每条有界量词都以 `q` 处的值的成员为界，两个参数位置在每条约束下各移一位，故内层读式照旧把新变元当作位置零来称呼。

第一条子句以 `var q` 的成员为界作存在量化，体为 `sglAt zero (suc u)`：位置零上的新变元是候选成员，而 `suc u` 是 `u` 经移位后的位置。第二条子句用 `pairAt` 同理，此刻同时提到 `u` 与 `v` 移位后的位置。第三条子句以全称量词为界，其体是两条读式的析取：`q` 处之值的每个成员仅仅是单点集或对。存在见证与「二者居其一」的分类保持命题截断，与 `SglOf` 和 `PairOf` 中完全一致；对象语言不选取成员，只说仅仅存在一个。

```agda
prAt : ∀ {n} → Fin n → Fin n → Fin n → Formula (V ℓ) n
prAt q u v = (∃̇∈ (var q) (sglAt zero (suc u)))
          ∧̇ ((∃̇∈ (var q) (pairAt zero (suc u) (suc v)))
          ∧̇ (∀̇∈ (var q) (sglAt zero (suc u) ∨̇ pairAt zero (suc u) (suc v))))

Δ₀-prAt : ∀ {n} (q u v : Fin n) → Δ₀ (prAt q u v)
```

有界性由语法给出证书。检查器 `checkΔ₀` 遍历组装后的公式，由于每个节点都是原子、联结词或以变元为界的量词，它以平凡的证书 `tt` 接受，得到 `Δ₀-prAt`。这把该读式放入那个有界类，其满足关系在传递模型之间是绝对的，后续关于绝对性的各章正依赖这一点。

```agda
Δ₀-prAt q u v = checkΔ₀ (prAt q u v) tt
```

## 充分性

最后的定理把对象语言的读式与其外部含义连接起来。由于满足关系取值于 `hProp`，这条陈述本身就是真值之间的一条路径：命题 `γ ⊨ prAt q u v` 被等同于「`q` 处的值等于 `u` 与 `v` 处之值的 Kuratowski 对」这一命题，并附上该相等类型为命题的证明，因为 `V ℓ` 是 h-集合。展开三条联结词与有界量词的满足关系后，左边恰好变成 `prChar-fwd` 与 `prChar-bwd` 所消耗的三条假设，于是充分性证明只是把两个已有论证组合起来，而不需证明任何新东西。

所展示的路径两侧都是真值。右边把相等类型 `⟦ var q ⟧ γ ≡ pr (⟦ var u ⟧ γ) (⟦ var v ⟧ γ)` 与 `setIsSet _ _` 配对，后者是「两个 h-集合元素的相等是命题」的证明；这种配对正是构造 `hProp` 的方式。证明随后给出底层当且仅当的两个方向，`⇔toPath` 把它们提升为命题间的路径。

```agda
prAt-adequate : ∀ {n} (q u v : Fin n) (γ : (V ℓ) ^ n)
              → (γ ⊨ prAt q u v) ≡ ((⟦ var q ⟧ γ ≡ pr (⟦ var u ⟧ γ) (⟦ var v ⟧ γ))
                                   , setIsSet _ _)
prAt-adequate q u v γ = ⇔toPath
  (λ { (h₁ , h₂ , h₃) → prChar-fwd _ _ _ h₁ h₂ h₃ })
```

前进方向接收 `prAt q u v` 的满足关系，按 `_∧̇_` 与有界的 `∃̇∈`、`∀̇∈` 的语义，它是一个三元组：满足单点集读式的成员的截断存在、满足对读式的成员的截断存在，以及全称条款。这恰是 `prChar-fwd` 的三个参数，它们返回到 `pr U W` 的路径。反向取这条相等路径交给 `prChar-bwd`，后者把它包装成语义重新组装为满足关系的三条子句。两个方向都没有检查任何集合是如何构造的。

```agda
  (λ e → prChar-bwd _ _ _ e)
```

## 小结

`prAt` 从对象语言内部读出 Kuratowski 对，它是 Δ₀ 的且是充分的，其满足关系是一条通往「与指派值之 `pr` 相等」的路径。解构一个码所需的全部证书信息，如今都已具有有界形式，既不使用递归，也不比较码值。随后诸章在这些读式的基础上构造证书。