---
title: "经典逻辑的边界"
module: Base.Classical
lang: zh
site: "Bedrock"
description: "经典逻辑的边界"
stage: "基础"
reading_order: 4
canonical: https://bedrock.institute/zh/Base.Classical.html
html: Base.Classical.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/Base/Classical.lagda.md
prerequisites: [Base.Prelude, Base.Impredicativity]
routes: [common-foundations]
translations: [https://bedrock.institute/en/Base.Classical.md, https://bedrock.institute/ja/Base.Classical.md]
agent_guide: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---
```agda
{-# OPTIONS --cubical --safe --guardedness #-}
module Base.Classical where
```
# 经典逻辑的边界
```agda
open import Base.Prelude
open import Base.Impredicativity
using ( Resizing; ΩResizing; ΩResizing→Resizing )
```
本书以构造主义的 Cubical 类型论为基础，在其中发展经典集合论。保留构造主义的基础，可以清楚划出经典推理的边界：不需要排中律的定义和证明仍然是构造主义的；真正需要排中律的定理，则把它作为显式参数。如果一开始就在基础理论中预设经典逻辑，定理的陈述本身就无法再显示这种区别。
排中律不仅标志着本书进入经典推理之处，还能解决上一章留下的两个命题大小问题：
- 命题换级：给定 `P : hProp ℓ₁`，能否在指定层级 `ℓ₂` 找到一个命题，使其底层类型与 `P` 的底层类型等价？
- 命题宇宙换级：能否用 `Type ℓ₂` 中的单一类型呈现整个 `hProp ℓ₁`？
## 排中律
排中律为每个命题给出真假的判定。命题分居不同的宇宙，因此这条原理需要逐层陈述。
**定义** (`LEM`) 我们把「`ℓ` 层的排中律」记作 `LEM ℓ`，并将其定义为以下依值函数：对每个 `P : hProp ℓ`，它返回判定 `Dec ⟨ P ⟩`；`yes` 携带 `P` 的证明，`no` 则携带它的反驳。由于这个函数量化整个命题宇宙 `hProp ℓ`，`LEM ℓ` 位于 `Type (ℓ-suc ℓ)`。它的层级指标因而准确标明了这项经典假设可以判定哪些命题。
```agda
LEM : ∀ ℓ → Type (ℓ-suc ℓ)
LEM ℓ = (P : hProp ℓ) → Dec ⟨ P ⟩
```
**事实** (`isPropLEM`) 对每个层级 `ℓ`，排中律 `LEM ℓ` 本身也是命题。
```agda
isPropLEM : ∀ {ℓ} → isProp (LEM ℓ)
```
**证明** 对每个 `P : hProp ℓ`，`isPropDec` 说明 `Dec ⟨ P ⟩` 是命题。再由命题对依赖函数的封闭性 `isPropΠ` 逐点证明结论。
```agda
isPropLEM {ℓ} = isPropΠ λ P → isPropDec ⟨ P ⟩isProp
```
**引理** (`lowerLEM`) 后继层级上的排中律蕴含紧邻低一层的排中律。反复应用该引理，即可继续逐层下降。
```agda
lowerLEM : ∀ {ℓ} → LEM (ℓ-suc ℓ) → LEM ℓ
```
**证明** 给定 `lem : LEM (ℓ-suc ℓ)`，并固定 `P : hProp ℓ`。`lem` 要求输入 `ℓ-suc ℓ` 层的命题，因而不能直接判定 `P`。为此，构造一个高层命题：其底层类型是 `Lift ⟨ P ⟩`，命题性证书是 `isOfHLevelLift 1 ⟨ P ⟩isProp`。把这一对交给 `lem`，便得到 `P` 的抬升副本的判定。
下图的两个分支说明如何把这一判定转回 `Dec ⟨ P ⟩`：肯定分支使用 `lower`，否定分支则假设 `P` 的证明，并反驳其抬升后的像。函数 `mapDec` 把这两种转换合在一起。
```agda
lowerLEM {ℓ} lem P =
mapDec lower (λ np p → np (lift p))
(lem (Lift ⟨ P ⟩ , isOfHLevelLift 1 ⟨ P ⟩isProp))
```
$$\operatorname{yes}\,\hat x$$
$\operatorname{Lift}\langle P\rangle$
$\hat x$
$\operatorname{lower}$
$\langle P\rangle$
$\operatorname{lower}\,\hat x$
$$\operatorname{yes}\,(\operatorname{lower}\,\hat x)$$
$$\operatorname{no}\,\mathit{np}$$
$\operatorname{Lift}\langle P\rangle$
$\operatorname{lift}\,p$
$\operatorname{lift}$
$\langle P\rangle$
$p$
$$\mathit{np}\,(\operatorname{lift}\,p):\bot_0$$
肯定判定通过 `lower` 把证明向下搬移。否定判定则临时假设 `p : ⟨ P ⟩`，经 `lift` 向上搬移，再由 `np` 得到矛盾
## 由排中律得到命题宇宙换级
一旦源层的每个命题都可以判定，就能用两个布尔标签之一来代表它。对任意层级 `ℓ₁` 与 `ℓ₂`，`ΩResizing ℓ₁ ℓ₂` 要求 `Type ℓ₂` 中有一个与整个 `hProp ℓ₁` 类型等价的类型。本章从 `ℓ₁` 层的排中律构造这样的分类器，再应用一般定理 `ΩResizing→Resizing`，把这个对命题宇宙的小表示转化为 `Resizing ℓ₁ ℓ₂`：源层的每个命题在目标层都有一个与之类型等价的代表。
分类器采用前文引入的类型 `Bool`，以它的两个构造子 `true` 与 `false` 作为标签。
这些标签只是编码，并非 `hProp ℓ₁` 中的命题。`Bool` 位于 `Type ℓ-zero`，所以要把编码类型提升为目标宇宙 `Type ℓ₂` 中的 `Lift {ℓ-zero} {ℓ₂} Bool`。它的两个标签将分别代表 `hProp ℓ₁` 中的 `⊤` 与 `⊥`，而这两个命题可用于任意层级。只要构造出这个目标层编码类型与命题宇宙之间的等价，就得到了所需的命题宇宙换级。
构造分为两步。第一步先根据显式判定 `Dec ⟨ P ⟩` 定义编码，再定义解码，最后证明两条往返律。我们把这四项辅助结果放在私有子模块 `BooleanCodes` 中，它们都不使用排中律。第二步的公开定理才调用排中律，为每个 `P` 统一给出判定，并把这四项结果组装成所需的等价。
```agda
private module BooleanCodes where
```
**引理** (`encodeB`) 存在一个编码操作，它以命题 `P` 及其判定为输入，返回 `Lift {ℓ-zero} {ℓ₂} Bool` 中的编码。
```agda
encodeB : ∀ {ℓ₁ ℓ₂} (P : hProp ℓ₁) → Dec ⟨ P ⟩ → Lift {ℓ-zero} {ℓ₂} Bool
```
**证明** 考察给定的判定。`yes` 分支返回 `lift true`，`no` 分支返回 `lift false`。两个分支都舍去具体的证明或反驳，只保留哪一种结果成立。由于判定是显式给出的，编码过程不使用排中律。
```agda
encodeB P (yes _) = lift true
encodeB P (no _) = lift false
```
**引理** (`decodeB`) 存在一个解码操作，它以 `Lift {ℓ-zero} {ℓ₂} Bool` 中的编码为输入，返回 `hProp ℓ₁` 中的命题。
```agda
decodeB : ∀ {ℓ₁ ℓ₂} → Lift {ℓ-zero} {ℓ₂} Bool → hProp ℓ₁
```
**证明** 考察给定的编码。`lift true` 分支返回 `⊤`，`lift false` 分支返回 `⊥`。两个分支都舍去标签，只保留它所代表的命题。由于两种情形都是直接给出的，解码过程同样不使用排中律。
```agda
decodeB (lift true) = ⊤
decodeB (lift false) = ⊥
```
**引理** (`secB`) 对任意命题 `P` 及其判定 `d`，先用 `encodeB` 编码，再用 `decodeB` 解码，会在 `hProp` 中恢复 `P`：`decodeB (encodeB P d) ≡ P`。
```agda
secB : ∀ {ℓ₁ ℓ₂} (P : hProp ℓ₁) (d : Dec ⟨ P ⟩)
→ decodeB {ℓ₁} {ℓ₂} (encodeB {ℓ₁} {ℓ₂} P d) ≡ P
```
**证明** 对 `d` 分情形。若 `d = yes p`，编码选出 `lift true`，解码得到 `⊤`，所以目标化为 `⊤ ≡ P`。命题外延性 `⇔toPath` 从两个方向的映射构造这条路径：一个映射返回 `p`，另一个映射返回 `tt*`。若 `d = no np`，编码选出 `lift false`，解码得到 `⊥`，所以目标化为 `⊥ ≡ P`。两个方向的映射分别是荒谬函数 `λ ()`，以及先应用反驳 `np`、再从 `⊥₀` 消去的函数。因此在两种情形下，先编码再解码都会恢复一个与 `P` 相等的命题。
```agda
secB {ℓ₁} {ℓ₂} P (yes p) = ⇔toPath (λ _ → p) (λ _ → tt*)
secB {ℓ₁} {ℓ₂} P (no np) = ⇔toPath (λ ()) (λ p → ⊥₀-rec (np p))
```
**引理** (`retrB`) 对任意编码 `b̂` 及其解码所得命题的判定 `d`，先用 `decodeB` 解码，再用 `encodeB` 编码，会恢复 `b̂`：`encodeB (decodeB b̂) d ≡ b̂`。
```agda
retrB : ∀ {ℓ₁ ℓ₂} (b̂ : Lift {ℓ-zero} {ℓ₂} Bool)
(d : Dec ⟨ decodeB {ℓ₁} {ℓ₂} b̂ ⟩)
→ encodeB {ℓ₁} {ℓ₂} (decodeB {ℓ₁} {ℓ₂} b̂) d ≡ b̂
```
**证明** 先对 `b̂` 分情形，再对 `d` 分情形，共有四种组合。若 `b̂ = lift true`，解码得到 `⊤`。证明会再次选出 `lift true`，所以等式由 `refl` 成立；反驳则不可能存在，因为把它用于 `tt*` 就会得到 `⊥₀` 的元素。若 `b̂ = lift false`，解码得到 `⊥`。证明因空模式 `()` 而不可能；反驳会再次选出 `lift false`，所以等式也由 `refl` 成立。因此在所有可能的情形下，先解码再编码都会恢复原编码。
```agda
retrB {ℓ₁} {ℓ₂} (lift true) (yes _) = refl
retrB {ℓ₁} {ℓ₂} (lift true) (no n⊤) = ⊥₀-rec (n⊤ tt*)
retrB {ℓ₁} {ℓ₂} (lift false) (yes ())
retrB {ℓ₁} {ℓ₂} (lift false) (no _) = refl
```
两条往返律共同表明：只要能为每个命题统一给出判定，编码与解码就互为逆映射。因此，所得分类器将给出真正的类型等价，而不只是用两个真值标签满射地覆盖命题。
候选见证是序对 `(Lift Bool , ...)`：第一分量位于 `Type ℓ₂`，第二分量将是类型等价 `hProp ℓ₁ ≃ Lift Bool`。这里不要求 `ℓ₁` 与 `ℓ₂` 具有任何大小关系。后文使用的向下实例取 `ℓ₁ = ℓ-suc ℓ`、`ℓ₂ = ℓ`，但目标层级也可以与源层级相同或更高。排中律只剩下一项作用：为编码器统一提供所需的判定；以上四项私有结果都是构造主义的。
**定理** (`LEM→ΩResizing`) 对任意层级 `ℓ₁` 与 `ℓ₂`，源层 `ℓ₁` 的排中律蕴含从 `ℓ₁` 到 `ℓ₂` 的命题宇宙换级。
```agda
LEM→ΩResizing : ∀ {ℓ₁ ℓ₂} → LEM ℓ₁ → ΩResizing ℓ₁ ℓ₂
```
**证明** 取 `Lift Bool` 为第一分量。第二分量使用 `isoToEquiv`，把下面的同构转化为类型等价。同构的正向映射把 `P` 送到 `encodeB P (lem P)`，逆向映射是 `decodeB`；两条往返律分别使用 `retrB` 与 `secB`，并以 `lem` 给出的判定将其具体化。这两个分量共同构成 `ΩResizing ℓ₁ ℓ₂` 所需的见证。
```agda
LEM→ΩResizing lem = Lift Bool , isoToEquiv (iso
(λ P → encodeB P (lem P)) decodeB
(λ b → retrB {ℓ₁ = _} b (lem (decodeB b)))
(λ P → secB {ℓ₂ = _} P (lem P)))
where open BooleanCodes
```
下图中的两个三角形分别由两条往返律闭合。固定 `lem : LEM ℓ₁`，把编码类型 `Lift {ℓ-zero} {ℓ₂} Bool` 简写为 $B$，并记 $E(P) := \operatorname{encodeB}\,P\,(\operatorname{lem}\,P)$、$D := \operatorname{decodeB}$。每次往返所得的点，都由标出的路径与出发点相连。
$B$
$E(P)$
$\operatorname{hProp}\,\ell_1$
$P$
$D(E(P))$
$E$
$D$
$\operatorname{secB}$
$\operatorname{hProp}\,\ell_1$
$D(b)$
$B$
$b$
$E(D(b))$
$D$
$E$
$\operatorname{retrB}$
编码与解码在路径意义下互为逆映射。排中律为 $E$ 提供判定；给定显式判定后，编码、解码与两条往返律都是构造主义的
**推论** (`LEM→Resizing`) 对任意层级 `ℓ₁` 与 `ℓ₂`，源层 `ℓ₁` 的排中律蕴含从 `ℓ₁` 到 `ℓ₂` 的命题换级。
**证明** 先应用 `LEM→ΩResizing` 得到命题宇宙换级，再用一般定理 `ΩResizing→Resizing` 将其转化为命题换级。
```agda
LEM→Resizing : ∀ {ℓ₁ ℓ₂} → LEM ℓ₁ → Resizing ℓ₁ ℓ₂
LEM→Resizing lem = ΩResizing→Resizing (LEM→ΩResizing lem)
```
## 小结
本章把排中律逐层写成 `LEM ℓ`，证明它本身是命题，并用 `lowerLEM` 从后继层级的排中律得到紧邻低一层的实例。给定 `LEM ℓ₁`，`LEM→ΩResizing` 对任意目标层级 `ℓ₂` 构造 `ΩResizing ℓ₁ ℓ₂`；再与 `ΩResizing→Resizing` 复合，便得到 `Resizing ℓ₁ ℓ₂`。因此，源层级上的同一个排中律假设解决了本章开头提出的两个大小问题。