---
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: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 经典逻辑的边界

在带宇宙层级的类型论中，命题引出两个不同的小性问题。第一，固定命题 `P : hProp (ℓ-suc ℓ)`，能否找到低一层宇宙中与之等价的命题？这就是命题降级：它逐个命题发言。第二，全体 `ℓ` 层命题的类型 `hProp ℓ` 本身住在 `Type (ℓ-suc ℓ)` 中；能否用一个小类型呈现整个总体？这就是小分类器。两项断言形状不同，本章由一条显式假设同时证明二者。

这条假设是排中律：给定层级的每个命题要么真要么假。Cubical 类型论并不预设它，因此这里的每个经典证明都把它作为显式参数接收，每项结果也准确记录所用的是哪个层级的实例。构造性定义与经典步骤全程分开：构造自身不作任何判定，假设只在消耗判定之处进入。

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

module Base.Classical where
```

两个小性问题已在「非直谓性」一章获得精确形状，本章原样使用那套词汇。对单个命题，`isSmall P` 由一个低层命题 `Q : hProp ℓ` 与底层类型间的等价 `⟨ P ⟩ ≃ ⟨ Q ⟩` 组成。两个统一陈述的区别在于量化的对象：`Resizing ℓ` 要求每个 `P : hProp (ℓ-suc ℓ)` 都带有这样的数据，而 `HPropSmallness ℓ` 要求一个与整个 `hProp ℓ` 同时等价的类型 `Ω' : Type ℓ`。前者是逐命题见证的族，后者是呈现总体的单一载体；本章从排中律分别导出二者，并且不断言二者之间有蕴含关系。

```agda
open import Base.Prelude
open import Base.Impredicativity
  using ( isSmall; Resizing; HPropSmallness; Impredicativity )
```

判定一个命题意味着什么，必须先于一切证明固定下来。判定 `P`，就是给出 `⟨ P ⟩` 的一个证明，或给出从 `⟨ P ⟩` 到空类型的映射：后者把任何证明都变成荒谬，从而反驳 `P`。余积 `_⊎_` 及其两个构造子承载的正是这种二选一，而且这个析取是真实的数据：元素知道自己来自哪一支，因此判定能够逐情形使用。布尔值 `Bool` 与 `true`、`false` 将为两种结果贴标签，`tt*` 则是「真」命题底层单元类型的唯一元素。

```agda
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Empty as Empty
open import Cubical.Data.Bool using ( Bool; true; false )
open import Cubical.Data.Unit using ( tt* )
```

小性通过「相同」来比较命题，下文会出现两种形式的相同。在两个命题之间，双向的一对映射既能经命题外延性 `⇔toPath` 给出 `hProp` 值之间的路径，也能经 `propBiimpl→Equiv` 给出底层类型间的等价。同构 `iso` 把两个映射与两条逆律一并记录，`isoToEquiv` 把它读作等价。分类器要等同命题，所以构造 `hProp` 的路径；命题降级要交付底层类型间的等价。

```agda
open import Cubical.Foundations.Equiv using ( propBiimpl→Equiv )
open import Cubical.Foundations.Isomorphism using ( iso; isoToEquiv )
open import Cubical.Functions.Logic using ( ⇔toPath )
```

## 陈述

在证明任何东西之前，必须先把假设连同其宇宙层级陈述清楚。层级指标不是装饰：它说明在哪个宇宙上要求统一判定，后续每个定理都在向读者交代它需要哪个经典实例。

对每个宇宙层级 `ℓ`，`LEM ℓ` 是一个函数：取命题 `P : hProp ℓ`，返回 `⟨ P ⟩` 的证明，或一个反驳，即从 `⟨ P ⟩` 映入空类型的映射。由于它量化了 `hProp ℓ` 的所有命题，其类型位于高一层宇宙 `Type (ℓ-suc ℓ)`。因此这个陈述本身是大的，尽管它产出的每个判定都只是一小段数据；而且 `LEM ℓ` 是逐层陈述的，不是同时对所有层级断言。注意这种形状给出的强度：判定是数据而非命题，所以从排中律假设出发，可以在证明与反驳两种情形之间作分支推理，而不只是断言二者之一存在。

```agda
LEM : ∀ ℓ → Type (ℓ-suc ℓ)
LEM ℓ = (P : hProp ℓ) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥)
```

应用需要在不止一个层级上的排中律，而证明拿到的往往只有高层实例 `LEM (ℓ-suc ℓ)`。一条下降引理补上这个缺口。它是恰好一步的结果，即 `LEM (ℓ-suc ℓ) → LEM ℓ`：要判定 `P : hProp ℓ`，在上一层宇宙判定 `P` 的抬升副本，再把裁决带回。这里不声称判定可以一次跨越任意多层下降。

给定 `lem : LEM (ℓ-suc ℓ)` 与命题 `P : hProp ℓ`，计划不是把 `lem` 用在 `P` 本身上，而是用在住在 `ℓ-suc ℓ` 层、因而假设可适用的 `P` 的抬升副本上，然后再把关于副本的裁决翻译回关于 `P` 的裁决。

```agda
lowerLEM : ∀ {ℓ} → LEM (ℓ-suc ℓ) → LEM ℓ
lowerLEM {ℓ} lem P = fromLifted (lem lifted)
```

抬升后的命题底层类型为 `Lift ⟨ P ⟩`，其元素就是高一层宇宙中的 `⟨ P ⟩` 元素，而且它是命题：对元素 `x` 与 `y`，先用 `lower` 把二者降到 `⟨ P ⟩`，用 `P` 的命题性 `P .snd` 得到降像之间的路径，再用 `cong lift` 把该路径抬回上层。于是 `lifted` 是 `lem` 的合法输入。

```agda
  where
  lifted : hProp (ℓ-suc ℓ)
  lifted = Lift ⟨ P ⟩ , λ x y → cong lift (P .snd (lower x) (lower y))
```

翻译裁决只需要 `lift` 与 `lower`，而它们的方向恰好合适。`Lift ⟨ P ⟩` 的证明经 `lower` 降为 `⟨ P ⟩` 的证明；`Lift ⟨ P ⟩` 的反驳与 `lift` 复合后成为 `⟨ P ⟩` 的反驳，因为它在抬升之后适用于 `⟨ P ⟩` 的任何证明。两种情形都是判定的纯粹搬运，自身不含经典推理；经典的步骤是判定那个抬升后的命题。

```agda
  fromLifted : ⟨ lifted ⟩ ⊎ (⟨ lifted ⟩ → Empty.⊥) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥)
  fromLifted (inl p)  = inl (lower p)
  fromLifted (inr np) = inr (λ p → np (lift p))
```

## 由排中律得到小分类器

在经典观点下，固定层级的每个命题只有两种可能：真或假。这提示了一个两点的分类器。小代表取 `Lift Bool`，其中 `true` 代表命题「真」，`false` 代表命题「假」。有两点提醒使图景保持准确。布尔值只是标签；它所代表的命题是另一个 `hProp` 值，分类器只按 `hProp` 值之间的路径把它们等同，绝不按语法上的同一。并且两端大小不同：`Lift Bool` 住在 `Type ℓ`，而 `hProp ℓ` 住在 `Type (ℓ-suc ℓ)`；等价可以联系不同层级的类型，这个大小差正是所要建立的小性。

构造分成干净的两步。解码把每个布尔值送到它代表的命题。编码则需要知道给定的 `P` 属于哪种情形，因此把 `P` 的判定作为显式参数；两条逆律随后针对这份数据证明。排中律只在最后出现，用于一致地供给这些判定。

两个代表命题是《基础词汇》逻辑运算中典范的顶命题 `⊤` 与底命题 `⊥`。后者按定义就是对 `(⊥* , isProp⊥*)`，因此其底层类型是空类型 `⊥*`。二者在任意层级 `ℓ` 都可用，这正是它们能在 `hProp ℓ` 内部充任代表的原因；下面的布尔标签指称的恰是这两个命题。

```agda
private
  decodeB : ∀ {ℓ} → Lift {ℓ-zero} {ℓ} Bool → hProp ℓ
```

解码读取布尔标签，返回它所代表的命题：`lift true` 给出 `⊤`，`lift false` 给出 `⊥`。定义域是提升 `Lift {ℓ-zero} {ℓ} Bool` 而非 `Bool` 本身：`Bool` 住在 `Type ℓ-zero`，其提升是 `Type ℓ` 中的类型，这正是分类器陈述所要求的。注意，单独的解码只是一个指派代表的函数；这个指派在两个方向上都忠实，是下面两条逆律的内容。

```agda
  decodeB (lift true)  = ⊤
  decodeB (lift false) = ⊥
```

编码是相反方向的指派：给定 `P` 与 `P` 的一个判定，返回获胜情形的标签。判定是显式参数而非编码器自己产出的，所以这一步不使用排中律。一般而言，为 `P` 选代表是两步的事：先判定 `P`，再读出标签。两条逆律将表明这两趟往返各自是恒等，一趟在命题上，一趟在标签上。

匹配对象是判定而非 `P`：左支的元素给出 `lift true`，右支的元素给出 `lift false`。证明或反驳本身被丢弃，因为标签只记录出现的是哪种情形，而不是见证。结果类型是 `Lift {ℓ-zero} {ℓ} Bool`，与 `decodeB` 的定义域严格相配。

```agda
  encodeB : ∀ {ℓ} (P : hProp ℓ) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥) → Lift {ℓ-zero} {ℓ} Bool
  encodeB P (inl _) = lift true
  encodeB P (inr _) = lift false
```

第一条逆律说，经由判定选出的代表与 `P` 有相同的真值。具体地，`secB` 证明 `decodeB (encodeB P d) ≡ P`，这是 `hProp` 值之间的一条路径。两种情形的证明策略相同：给出双向的映射，再由命题外延性 `⇔toPath` 组装出路径。

若判定是证明 `p`，目标是 `⊤ ≡ P`。从 `⊤` 到 `⟨ P ⟩` 的映射就是判定所得的见证 `p`；反方向上，所有输入都映到 `⊤` 的唯一元素 `tt*`。若判定是反驳 `np`，目标是 `⊥ ≡ P`。从 `⊥*` 出发没有构造子可匹配，荒谬模式 `λ ()` 表达的正是这一点；`⟨ P ⟩` 的每个证明 `p` 都交给 `np` 并由 `Empty.rec` 消去。两个分支中，所选代表都与 `P` 路径相等，于是编码的往返不丢失任何真值。

```agda
  secB : ∀ {ℓ} (P : hProp ℓ) (d : ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥))
       → decodeB (encodeB P d) ≡ P
  secB P (inl p)  = ⇔toPath (λ _ → p) (λ _ → tt*)
  secB P (inr np) = ⇔toPath (λ ()) (λ p → Empty.rec (np p))
```

第二条逆律把代表读回来：`encodeB (decodeB b) d ≡ b`。这里有个关键细节。在组装好的分类器中，判定 `d` 将由排中律产生，而任何东西都不保证那个判定如何计算。所以 `retrB` 必须对**每一个**判定 `d` 成立，而不是只对某个特定证明会供给的判定成立。证明因此分成四种情形：两个相容的分支计算为 `refl`，两个不相容的分支作为不可能而消去；这也表明两个代表不会被混淆，因为 `⊤` 有元素而 `⊥` 为空。

当 `b = lift true` 时，解码得 `⊤`。配以证明编码返回 `lift true`，目标按定义就是 `refl`。所谓反驳的分支不可能出现：把它用于 `⊤` 的元素 `tt*` 会得到空类型的元素，`Empty.rec` 便由这一矛盾结案。

```agda
  retrB : ∀ {ℓ} (b : Lift {ℓ-zero} {ℓ} Bool)
          (d : ⟨ decodeB b ⟩ ⊎ (⟨ decodeB b ⟩ → Empty.⊥))
        → encodeB (decodeB b) d ≡ b
  retrB (lift true)  (inl _)  = refl
  retrB (lift true)  (inr n⊤) = Empty.rec (n⊤ tt*)
```

当 `b = lift false` 时，解码得 `⊥`，其底层类型为 `⊥*`。它的所谓证明将是空类型的项，荒谬模式 `()` 立即结束该分支；配以反驳编码返回 `lift false`，同样由 `refl` 完成。纵观四种情形，无论供给哪种判定，返回的标签总等于出发时的标签。

```agda
  retrB (lift false) (inl ())
  retrB (lift false) (inr _)  = refl
```

现在各部分组装成 `HPropSmallness ℓ` 所承诺的分类器：一个 `Type ℓ` 中的、与 `hProp ℓ` 等价的类型。小类型是 `Lift Bool`；等价来自这样的同构：正向映射是 `decodeB`，反向映射判定 `P` 后编码。两条逆律正是 `secB` 与 `retrB`，各自用来自 `lem` 的判定实例化。排中律在本节的作用就在此处：它一致地供给那些构造性部分作为输入所需的判定。

对子 `(Lift Bool , ...)` 是 `HPropSmallness ℓ` 的见证：第一分量类型为 `Type ℓ`，第二分量是等价 `Lift Bool ≃ hProp ℓ`。层级安排正是要点：`Lift Bool` : `Type ℓ` 而 `hProp ℓ` : `Type (ℓ-suc ℓ)`，于是高一宇宙的类型获得了一个小代表。这是关于宇宙层级的尺寸陈述，不是声称两端共享同一个宇宙；而且等价本身依赖两条逆律，因此布尔标签与其命题只是在 `secB` 与 `retrB` 所认证的路径之下被等同。

```agda
lem→hPropSmallness : ∀ {ℓ} → LEM ℓ → HPropSmallness ℓ
lem→hPropSmallness lem = Lift Bool , isoToEquiv (iso decodeB
  (λ P → encodeB P (lem P))
  (λ P → secB P (lem P))
  (λ b → retrB b (lem (decodeB b))))
```

## 由排中律得到命题降级

第二个小性问题是逐命题的。固定 `P : hProp (ℓ-suc ℓ)`，命题降级产出命题 `Q : hProp ℓ` 以及底层类型间的等价 `⟨ P ⟩ ≃ ⟨ Q ⟩`。同样的两个代表再次可用：若 `P` 为真取 `⊤`，若为假取 `⊥`，二者都在 `ℓ` 层。注意结果的形状：它是底层类型间的等价，而不是打包命题 `P` 与 `Q` 之间的路径。

两个构造的差别在于所组装的「相同」是什么。分类器要等同命题，所以它的相同由命题外延性组装为 `hProp` 值之间的路径。命题降级要交付的则是底层类型间的等价，`propBiimpl→Equiv` 恰好产出它：输入两侧的命题性证明 `P .snd` 与 `Q .snd` 连同两个映射，返回 `⟨ P ⟩ ≃ ⟨ Q ⟩`。

给定 `P` 的一个判定，`resizeDec` 返回 `isSmall P` 的见证。真情形的见证是 `(⊤ , 等价)`：从 `⟨ P ⟩` 到 `⊤` 的映射把所有输入映到 `tt*`，返回的映射使用判定所得的证明 `p`。由于两侧都是命题，`propBiimpl→Equiv` 在收到命题性证明 `P .snd` 与 `⊤ .snd` 后，把这组映射变成底层类型间的等价。

```agda
private
  resizeDec : ∀ {ℓ} (P : hProp (ℓ-suc ℓ)) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥)
            → isSmall P
  resizeDec P (inl p)  = ⊤ , propBiimpl→Equiv (P .snd) (⊤ .snd) (λ _ → tt*) (λ _ → p)
  resizeDec P (inr np) = ⊥ , propBiimpl→Equiv (P .snd) (⊥ .snd)
```

假情形的见证是 `(⊥ , 等价)`，映射与 `secB` 中的相同：从 `⟨ P ⟩` 出发的映射用反驳 `np` 经 `Empty.rec` 处理每个证明 `p`，反向映射则当场荒谬，因为 `⊥*` 没有构造子。两个代表 `⊤` 与 `⊥` 都住在比 `P` 低一层的 `ℓ` 层，这正是所要认证的小性：`Q` 取自 `hProp ℓ` 内部，等价连接 `⟨ P ⟩` 与 `⟨ Q ⟩`。

```agda
                               (λ p → Empty.rec (np p)) (λ ())
```

命题降级由此从 `ℓ-suc ℓ` 层级上排中律的一个实例得到，而这个层级是陈述自身规定的：`Resizing ℓ` 量化 `hProp (ℓ-suc ℓ)`，它消耗的判定恰是高一宇宙命题的判定。

`lem→resizing` 用一行把 `LEM (ℓ-suc ℓ)` 变为 `Resizing ℓ`：对每个 `P : hProp (ℓ-suc ℓ)`，用 `lem` 判定它，把裁决交给 `resizeDec`。关键全在层级的方向：`ℓ` 层的命题降级消耗 `ℓ-suc ℓ` 层的经典判定，因为获得低层等价代表的命题恰好是高一宇宙中的那些。

```agda
lem→resizing : ∀ {ℓ} → LEM (ℓ-suc ℓ) → Resizing ℓ
lem→resizing lem P = resizeDec P (lem P)
```

## 合并两项结论

两项尺寸控制现在来自同一条假设。`LEM (ℓ-suc ℓ)` 的一个实例直接给出命题降级，又经 `lowerLEM` 下降一步给出小分类器。两条原理仍是不同的陈述：本章从同一假设证明二者，但对其中一条是否蕴含另一条不作断言。

「非直谓性」一章中的记录 `Impredicativity ℓ` 有两个字段，每条原理各一个，而 `lem→impredicativity` 用同一个 `lem` 填满两者。命题降级字段是 `lem→resizing lem`，在该实例自身的层级上使用它。分类器字段是 `lem→hPropSmallness (lowerLEM lem)`，先降到 `LEM ℓ`，再构造 `Lift Bool ≃ hProp ℓ`。共享是关于这个推导的事实：两项结论都从同一个高层实例可证，而不是宣称两条原理相互蕴含。

```agda
lem→impredicativity : ∀ {ℓ} → LEM (ℓ-suc ℓ) → Impredicativity ℓ
lem→impredicativity lem = record
  { resizing       = lem→resizing lem
  ; hPropSmallness = lem→hPropSmallness (lowerLEM lem) }
```

## 小结

本章中的排中律只有一件事：在给定层级上判定每个命题的能力，且始终作为显式假设传递。一个 `ℓ-suc ℓ` 实例供给了全章所需的判定。它为 `lowerLEM` 判定各个抬升命题，为命题降级判定各个 `P : hProp (ℓ-suc ℓ)`，又经一步下降，为小分类器判定每个 `P : hProp ℓ`。两项推论仍是不同的原理，本章未对二者作任何比较；`lem→impredicativity` 同时持有二者，是因为同一条假设恰好给出了二者。累积层级诸章将接过这一接口，在全分离与 `V` 的幂集背后需要小性的地方加以使用。