形式化方法导引系列的主线问题是：“为什么编译通过就是定理得证”。要把这条等式撑起来，第一步是回答一个看似更基本的问题：什么算一个证明。

中学数学里"证明"通常意味着一段以"证："开头、以"证毕"结束的自然语言论证。这种证明里允许使用反证法、双否定消去、排中律，论证的合法性靠人类同行评议把关。这条路线下，"证明"是一份可被阅读和判断的文档。

形式化系统走另一条路。证明被要求成为一个可以被机械构造、机械检查的对象。这条要求一旦贯彻到底，传统数学里的"反证"和"排中"会被部分剥离，剩下一种叫直觉主义逻辑或构造主义逻辑的子系统。BHK 解释（Brouwer-Heyting-Kolmogorov）正是把"证明"在这个子系统里重新定义成"构造一个见证物"的规范。

本篇展开 BHK 翻译表，解释为什么它天然导向 Curry-Howard 同构，并用 Python 把表里的每一条编码成一个数据类。

古典逻辑与直觉主义逻辑的分歧

考虑一条最简单的古典定理：

存在两个无理数 a、b，使得 a^b 是有理数。

经典反证：考虑 sqrt(2) ^ sqrt(2)。如果它是有理数，取 a = b = sqrt(2) 即可；如果它是无理数，取 a = sqrt(2)^sqrt(2)、b = sqrt(2)，则 a^b = sqrt(2)^2 = 2，是有理数。无论哪种情况，命题成立。

这段证明在古典逻辑下完全合法。问题在于：它没有告诉读者到底是哪一组 (a, b)。论证依赖排中律——“要么 sqrt(2)^sqrt(2) 是有理数，要么不是”——而对哪种情形真正发生不作回答。

直觉主义视角拒绝这种"不指明见证就声称存在"的证明。构造主义者要求：

要证明 ∃x. P(x)，必须给出一个具体的 x，并附上 P(x) 的证明。

整条逻辑在这种要求下被重新过滤：

原则 古典逻辑 直觉主义逻辑
排中律 P ∨ ¬P 公理 不被普遍接受
双否定消去 ¬¬P → P 公理 不普遍成立
反证法 标准手段 只在证 ¬P 时合法
∃x. P(x) 可以非构造性声明 必须给出见证
P ∨ Q 可以由 ¬(¬P ∧ ¬Q) 推出 必须明确指出哪一支成立

直觉主义逻辑不是"古典逻辑的扩展"，而是"古典逻辑的子系统"：它能证明的命题是古典逻辑能证明命题的真子集，但它证明的每一条命题都附带一个见证物。

这一点是形式化系统选择直觉主义为内核的根本原因：见证物可以是程序，程序可以被类型系统检查。

BHK 解释：把每条联结词翻译成"构造方法"

BHK 解释由 Brouwer、Heyting、Kolmogorov 在 20 世纪上半叶分别提出，给"什么是 φ 的证明"提供了一份按命题结构归纳的定义：

命题形式 一个证明是什么
⊥（恒假） 没有证明
原子命题 A 由系统给定，例如某条公理或假设
P ∧ Q 一对：P 的证明 与 Q 的证明
P ∨ Q 一个带标签的证明：(left, P 的证明) 或 (right, Q 的证明)
P → Q 一个方法：把 P 的任一证明转换成 Q 的一个证明
¬P P → ⊥ 的一个证明，即"把 P 的任一证明转换成 ⊥ 的证明"的方法
∀x : A, P(x) 一个方法：给定任意 x : A，产出 P(x) 的一个证明
∃x : A, P(x) 一对：一个具体的见证 x : A 与 P(x) 的一个证明

这张表里有几件事值得读者反复回味：

  1. “证明"被换成了"对象”。每条联结词的证明都是一个可命名、可传递、可拆开的东西。这件东西不是论证，而是数据。
  2. → 的证明是方法。直觉主义说"P → Q 成立"不是声明"P 真时 Q 也真"，而是给出一个把 P 的证明加工成 Q 的证明的具体过程。
  3. ¬P 没有特殊地位。它就是 P → ⊥。研究"否定"的工具就是研究"函数"的工具。
  4. ∃ 必须给见证。回看前面那条"存在两个无理数 a、b 使 a^b 有理"的古典证明：它在直觉主义下不算证明，因为没有给出 (a, b) 是哪一对。

任何熟悉 CS 课程的读者读到这张表都会有一个反应：这看起来就是一组类型！配对类型、和类型、函数类型、依值函数类型、依值积类型——下一篇 Curry-Howard 同构正式把这个直觉变成定理。

为什么排中律失守

直觉主义下 P ∨ ¬P 不能作为公理，原因在 BHK 解释下变得直接：

要证明 P ∨ ¬P，必须给出：

  • 一个 (left, P 的证明)，或者
  • 一个 (right, ¬P 的证明)。

如果对 P 一无所知，例如 P = "黎曼猜想"，目前没有任何方法构造出哪一支。古典逻辑允许"反正必有一支成立"，直觉主义要求"现在就指出是哪一支"。

排中律不是"被禁止"，而是"不被白送"。在某些具体情形下排中律可证：例如 P = (n = 0 ∨ n ≠ 0)，对自然数 n 这条总可以构造性判定。直觉主义只是拒绝把它当成万能公理。

工程上读者更熟悉的对照：

古典立场 工程对照
“存在解，但我不告诉你怎么找” 编译器告诉你 Object x = findIt()，但 findIt 抛出 UnsupportedOperationException
“P ∨ ¬P 总成立，但具体哪支不管” 函数签名是 Either<Yes, No>，但实现是 throw new Error("undecided")
双否定消去 ¬¬P → P 知道"不存在反例"，就声称"有正例"——但代码没给出来

直觉主义把这些情形剔除，剩下的命题都自带一段可运行的"构造代码"。

用 Python 把 BHK 解释编码出来

把 BHK 表用 Python 数据类落地，可以让"证明是数据"这件事变得肉眼可见。先准备命题骨架：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
from __future__ import annotations
from dataclasses import dataclass
from typing import Any, Callable, Generic, TypeVar, Union

P = TypeVar("P")
Q = TypeVar("Q")
A = TypeVar("A")


# 一对：P 的证明 与 Q 的证明
@dataclass(frozen=True)
class And(Generic[P, Q]):
    left: P
    right: Q


# 带标签的证明：要么是 InL(P)，要么是 InR(Q)
@dataclass(frozen=True)
class InL(Generic[P]):
    proof: P


@dataclass(frozen=True)
class InR(Generic[Q]):
    proof: Q


Or = Union[InL[P], InR[Q]]


# 一个方法：把 P 的证明转换成 Q 的证明
@dataclass(frozen=True)
class Implies(Generic[P, Q]):
    method: Callable[[P], Q]


# 没有构造子的类型，对应 ⊥
class Bottom:
    pass


# ¬P 就是 P → ⊥
Not = Implies[P, Bottom]


# 存在：一对，见证 + 性质的证明
@dataclass(frozen=True)
class Exists(Generic[A, P]):
    witness: A
    proof: P


# 全称：一个方法，对任意见证给出对应性质的证明
@dataclass(frozen=True)
class ForAll(Generic[A, P]):
    method: Callable[[A], P]

下面写两条小定理作为示范。

定理 1：P ∧ Q → Q ∧ P。BHK 解释里它的证明是"输入一对 (p, q)，输出 (q, p)"：

1
2
3
4
5
6
7
8
def and_swap(pair: And[P, Q]) -> And[Q, P]:
    return And(left=pair.right, right=pair.left)


# 验证：构造一个 P ∧ Q 的"证明"，应用 and_swap
sample: And[str, int] = And(left="proof_of_P", right=42)
swapped = and_swap(sample)
print(swapped)

输出：

1
And(left=42, right='proof_of_P')

and_swap 是一个普通函数，它的代码就是 P ∧ Q → Q ∧ P 的证明。

定理 2：(P → Q) → (Q → R) → (P → R)。这条等价于函数组合：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
R = TypeVar("R")


def compose_implications(
    pq: Implies[P, Q],
    qr: Implies[Q, R],
) -> Implies[P, R]:
    def method(p: P) -> R:
        return qr.method(pq.method(p))
    return Implies(method=method)


# 验证：把"P 证明"映成"长度"，再把"长度"映成"是否奇数"
pq = Implies(method=lambda s: len(s))
qr = Implies(method=lambda n: n % 2 == 1)
pr = compose_implications(pq, qr)
print(pr.method("proof_of_P"))   # len=10, 10 % 2 == 1 -> False
print(pr.method("p"))             # len=1, 1 % 2 == 1 -> True

输出：

1
2
False
True

证明的核心是 lambda p: qr.method(pq.method(p))——函数组合。古典逻辑里这条定理是一句口号，直觉主义里它是一段三行的代码。

反例：尝试在 Python 里写 P ∨ ¬P 的"通用证明"。它需要对任意 P，要么给出 InL(p: P)，要么给出 InR(np: Not[P])。P 是任意类型，构造 p: P 通常做不到，构造 np: P → Bottom 也做不到。这正好对应排中律在直觉主义里失守。

模式提炼

模式 内容
证明即对象 把"证明 P"理解成"构造一个属于 P 的对象"，而不是"写一段说服人的论证"
→ 即方法 蕴含的证明就是把前提证明加工成结论证明的程序
∃ 必须给见证 存在性主张必须附带一个具体的 x 和 P(x) 的证明
否定即归谬函数 ¬P 没有特殊地位，它就是 P → ⊥ 的证明
排中律不白送 P ∨ ¬P 在直觉主义下需要逐案构造，不能预设

这五条模式是后续所有文章的"地基"。后面 STLC、依值类型、归纳类型只是给这套地基补上类型规则、机械检查算法、足够丰富的类型构造子。

给读者的练习

  1. 用上面的数据类证明 (P ∧ Q) → P，并跑出输出。
  2. 用上面的数据类证明 P → (Q → P)。这条定理叫常函数律。
  3. 用上面的数据类证明 ¬¬¬P → ¬P。注意这条在直觉主义下成立，而 ¬¬P → P 不成立——尝试构造 ¬¬P → P 时会卡在什么地方？
  4. 想清楚：为什么 (P → ⊥) → ⊥ → P 也不可证？

练习答案的形态都是一个 Python 函数，函数体就是 BHK 意义下的证明。

衔接到下一篇

本篇把"证明"重新定义成"构造一个对象"。BHK 表里每条联结词都对应一个常见的数据类型——配对、标签和、函数、依值函数、依值对。这不是偶然。

下一篇正式给出 Curry-Howard 同构：把 BHK 表的每一行升级成命题与类型之间的一一对应，并把"证明检查"和"类型检查"对位。从那里开始，"形式化编译器编译通过就是定理得证"这条主线问题的第一层翻译就被打通了。

参考资料

  • L. E. J. Brouwer. Über die Bedeutung des Satzes vom ausgeschlossenen Dritten in der Mathematik, insbesondere in der Funktionentheorie. 1924.
  • Arend Heyting. Intuitionism: An Introduction. North-Holland, 1956.
  • Dirk van Dalen. Logic and Structure. Springer, 2013.（第 5 章"直觉主义逻辑"）
  • Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.
  • Stanford Encyclopedia of Philosophy: Intuitionistic Logic.