h5i
本中文版由作者借助 AI 翻译而成。作者并非中文母语者，译文未经人工逐句校对，可能存在错误。如发现问题，请在 GitHub 上提交 issue。

附录 A

“证明即项”的证明

第 4 章断言，二阶命题逻辑中的每个证明都可以变成一个被内核接受的项（定理 4.1）。本附录把这一陈述精确化，并给出完整证明。一旦必要的簿记就位，证明并不长：它是对逻辑判断的推导做归纳，每种情形正好对应第 4 章表格中的一行，从左读到右。

思路

逻辑中的一棵推导是规则应用构成的树，而第 4 章的翻译把每条逻辑规则与一条类型规则配对，于是自然的计划是：从叶子向上遍历推导，在每个节点上构造配对的类型规则所给出的类型推导。假设变成变量查找，蕴涵引入变成 λ\lambda，蕴涵消去变成应用，两条量词规则则变成在 Sort 0\Sort{0} 上的 λ\lambda 和对类型的应用。

有两处细节需要留意，都和上下文有关。

  • 逻辑规则不说明哪些命题变量在作用域内，而类型这一侧需要知道，因为命题变量 PP 只有在假设 P:Sort 0P : \Sort{0} 进入上下文之后才能使用。因此精确陈述带有一个显式的命题变量列表 Θ\Theta。
  • 类型规则向右扩展上下文，而第 4 章的翻译 Δ∗\Delta^\ast 把所有命题变量放在所有假设之前。若允许任意交错，证明会更容易，所以我们对每个表示该逻辑判断的上下文证明定理，“表示”的含义见下文定义。

精确陈述

定理 4.1 没有明说哪些命题变量在作用域内；为了证明，我们把它们显式写出，记

Θ;Δ⊢φ,\Theta; \Delta \vdash \varphi,

其中 Θ\Theta 是互不相同的命题变量的列表，并且在 Δ\Delta 或 φ\varphi 中自由出现的每个命题变量都属于 Θ\Theta。带上这套簿记，第 4 章的规则读作如下。

φ∈ΔΘ;Δ⊢φ;(Hyp)Θ;Δ,φ⊢ψΘ;Δ⊢φ→ψ;(→-intro)Θ;Δ⊢φ→ψΘ;Δ⊢φΘ;Δ⊢ψ;(→-elim)\dfrac{\varphi \in \Delta}{\Theta; \Delta \vdash \varphi}\rulename{Hyp} \qquad \dfrac{\Theta; \Delta, \varphi \vdash \psi}{\Theta; \Delta \vdash \varphi \to \psi}\rulename{$\to$-intro} \qquad \dfrac{\Theta; \Delta \vdash \varphi \to \psi \qquad \Theta; \Delta \vdash \varphi}{\Theta; \Delta \vdash \psi}\rulename{$\to$-elim}
Θ,P;Δ⊢φP∉ΘΘ;Δ⊢∀P. φ;(∀-intro)Θ;Δ⊢∀P. φFV(ψ)⊆ΘΘ;Δ⊢φ[P↦ψ];(∀-elim)\dfrac{\Theta, P; \Delta \vdash \varphi \qquad P \notin \Theta}{\Theta; \Delta \vdash \forall P.\,\varphi}\rulename{$\forall$-intro} \qquad \dfrac{\Theta; \Delta \vdash \forall P.\,\varphi \qquad \FV(\psi) \subseteq \Theta}{\Theta; \Delta \vdash \subst{\varphi}{P}{\psi}}\rulename{$\forall$-elim}

第 4 章的附加条件 P∉FV(Δ)P \notin \FV(\Delta) 现在由 P∉ΘP \notin \Theta 蕴涵：在 Δ\Delta 中自由出现的每个命题变量都在 Θ\Theta 中，而 PP 不在。公式在 α\alpha 等价意义下看待，所以约束的 PP 总可以改名以满足附加条件。与第 4 章一样，φ∗→ψ∗\varphi^\ast \to \psi^\ast 表示 Π(x:φ∗). ψ∗\tPi{x}{\varphi^\ast}{\psi^\ast}，其中 xx 是新鲜的。

第 4 章的上下文 Δ∗\Delta^\ast 先列出命题变量，再列出假设，但证明需要向右扩展上下文，所以允许任意顺序更为方便。

定义 A.1（表示）. 称上下文 Γ\Gamma 表示 (Θ;Δ)(\Theta; \Delta)，如果 ⊢Γ;ok\ctxok{\Gamma}，且 Γ\Gamma 由以下假设按某种顺序组成：对每个 P∈ΘP \in \Theta 有一个假设 P:Sort 0P : \Sort{0}，对每个 χ∈Δ\chi \in \Delta 有一个假设 h:χ∗h : \chi^\ast。

定理 A.2（定理 4.1 的精确形式）. 若 Θ;Δ⊢φ\Theta; \Delta \vdash \varphi 且 Γ\Gamma 表示 (Θ;Δ)(\Theta; \Delta)，则存在项 tt 使得 Γ⊢t:φ∗\Gamma \vdash t : \varphi^\ast。

定理 4.1 是 Γ=Δ∗\Gamma = \Delta^\ast 的特例。当 Θ\Theta 列出全部自由命题变量时，上下文 Δ∗\Delta^\ast 恰好包含所需的假设；由下面的引理 A.3 加上规则 C-Ext，它是良构的，因为一旦命题变量在作用域内，每个假设类型 χ∗\chi^\ast 都是命题。

关于翻译的事实

翻译 φ↦φ∗\varphi \mapsto \varphi^\ast 与替换可交换：

(φ[P↦ψ])∗=φ∗[P↦ψ∗].(\subst{\varphi}{P}{\psi})^\ast = \subst{\varphi^\ast}{P}{\psi^\ast}.

这是对 φ\varphi 的例行归纳：两边都把 PP 的自由出现换成 ψ∗\psi^\ast，而翻译对命题变量什么也不做，只保留它的名字。主证明的 ∀\forall-elim 情形依赖这个等式。

下一条引理是第 13 章的宇宙结构唯一介入的地方，它说每个翻译后的公式都是命题，也就是类型为 Sort 0\Sort{0}。没有它，类型规则 T-Lam 就不能应用于假设，∀\forall-elim 情形也不能用任意公式实例化量词。

引理 A.3（公式是命题）. 若 ⊢Γ;ok\ctxok{\Gamma}，且对每个 P∈FV(φ)P \in \FV(\varphi) 都有 (P:Sort 0)∈Γ(P : \Sort{0}) \in \Gamma，则 Γ⊢φ∗:Sort 0\Gamma \vdash \varphi^\ast : \Sort{0}。

对 φ\varphi 归纳。

对命题变量 PP，假设给出 (P:Sort 0)∈Γ(P : \Sort{0}) \in \Gamma，于是由 T-Var 得 Γ⊢P:Sort 0\Gamma \vdash P : \Sort{0}。

对 φ→ψ\varphi \to \psi，归纳假设给出 Γ⊢φ∗:Sort 0\Gamma \vdash \varphi^\ast : \Sort{0}，于是对新鲜的 xx，由 C-Ext 知 Γ,x:φ∗\Gamma, x : \varphi^\ast 良构。在这个扩展后的上下文中对 ψ\psi 用归纳假设，得 Γ,x:φ∗⊢ψ∗:Sort 0\Gamma, x : \varphi^\ast \vdash \psi^\ast : \Sort{0}，再由 T-Pi 得 Γ⊢Π(x:φ∗). ψ∗:Sort imax(0,0)=Sort 0\Gamma \vdash \tPi{x}{\varphi^\ast}{\psi^\ast} : \Sort{\imax(0, 0)} = \Sort{0}。

对 ∀Q. χ\forall Q.\,\chi，把 QQ 改名使 Q∉dom(Γ)Q \notin \dom(\Gamma)。T-Sort 给出 Γ⊢Sort 0:Sort 1\Gamma \vdash \Sort{0} : \Sort{1}，于是由 C-Ext 知 Γ,Q:Sort 0\Gamma, Q : \Sort{0} 良构。在该上下文中对 χ\chi 用归纳假设，得 Γ,Q:Sort 0⊢χ∗:Sort 0\Gamma, Q : \Sort{0} \vdash \chi^\ast : \Sort{0}，再由 T-Pi 得 Γ⊢Π(Q:Sort 0). χ∗:Sort imax(1,0)=Sort 0\Gamma \vdash \tPi{Q}{\Sort{0}}{\chi^\ast} : \Sort{\imax(1, 0)} = \Sort{0}。

证明

我们对 Θ;Δ⊢φ\Theta; \Delta \vdash \varphi 的推导做归纳来证明定理 A.2，同时对所有表示它的上下文 Γ\Gamma 一并证明。每种情形构造的，都是第 4 章表格右栏所示的类型推导。

假设. 该规则由 φ∈Δ\varphi \in \Delta 得出 Θ;Δ⊢φ\Theta; \Delta \vdash \varphi。由于 Γ\Gamma 表示 (Θ;Δ)(\Theta; \Delta)，它包含一个假设 h:φ∗h : \varphi^\ast，于是由 T-Var 得 Γ⊢h:φ∗\Gamma \vdash h : \varphi^\ast。

→\to-intro. 前提是 Θ;Δ,φ⊢ψ\Theta; \Delta, \varphi \vdash \psi，结论是 Θ;Δ⊢φ→ψ\Theta; \Delta \vdash \varphi \to \psi。由引理 A.3，Γ⊢φ∗:Sort 0\Gamma \vdash \varphi^\ast : \Sort{0}。因此对新鲜的 hh，上下文 Γ,h:φ∗\Gamma, h : \varphi^\ast 由 C-Ext 良构，并且它表示 (Θ;Δ,φ)(\Theta; \Delta, \varphi)。把归纳假设用于该前提和这个上下文，得到对某个 tt 有 Γ,h:φ∗⊢t:ψ∗\Gamma, h : \varphi^\ast \vdash t : \psi^\ast，再由 T-Lam 得

Γ⊢λ(h:φ∗). t:Π(h:φ∗). ψ∗.\Gamma \vdash \tLam{h}{\varphi^\ast}{t} : \tPi{h}{\varphi^\ast}{\psi^\ast}.

这个类型就是 φ∗→ψ∗\varphi^\ast \to \psi^\ast：ψ∗\psi^\ast 的自由变量都是命题变量，hh 不在其中，所以 hh 不出现在 ψ∗\psi^\ast 里，这个 Π\Pi 是非依赖的。

→\to-elim. 前提是 Θ;Δ⊢φ→ψ\Theta; \Delta \vdash \varphi \to \psi 和 Θ;Δ⊢φ\Theta; \Delta \vdash \varphi。两个归纳假设给出 Γ⊢f:Π(x:φ∗). ψ∗\Gamma \vdash f : \tPi{x}{\varphi^\ast}{\psi^\ast}，其中 x∉FV(ψ∗)x \notin \FV(\psi^\ast)，以及 Γ⊢a:φ∗\Gamma \vdash a : \varphi^\ast。T-App 给出 Γ⊢f  a:ψ∗[x↦a]\Gamma \vdash f\;a : \subst{\psi^\ast}{x}{a}；由于 xx 不出现在 ψ∗\psi^\ast 中，替换什么也不做：ψ∗[x↦a]=ψ∗\subst{\psi^\ast}{x}{a} = \psi^\ast。

∀\forall-intro. 前提是 Θ,P;Δ⊢φ\Theta, P; \Delta \vdash \varphi，其中 P∉ΘP \notin \Theta；结论是 Θ;Δ⊢∀P. φ\Theta; \Delta \vdash \forall P.\,\varphi。必要时把 PP 改名，设 P∉dom(Γ)P \notin \dom(\Gamma)；一个例行归纳表明，把 Θ\Theta 中的变量改成新鲜变量保持推导不变。由 T-Sort 和 C-Ext，Γ,P:Sort 0\Gamma, P : \Sort{0} 良构，并且它表示 (Θ,P;Δ)(\Theta, P; \Delta)。归纳假设给出 Γ,P:Sort 0⊢t:φ∗\Gamma, P : \Sort{0} \vdash t : \varphi^\ast，再由 T-Lam 得

Γ⊢λ(P:Sort 0). t:Π(P:Sort 0). φ∗,\Gamma \vdash \tLam{P}{\Sort{0}}{t} : \tPi{P}{\Sort{0}}{\varphi^\ast},

这正是 ∀P. φ\forall P.\,\varphi 的翻译。

∀\forall-elim. 前提是 Θ;Δ⊢∀P. φ\Theta; \Delta \vdash \forall P.\,\varphi，其中 FV(ψ)⊆Θ\FV(\psi) \subseteq \Theta；结论是 Θ;Δ⊢φ[P↦ψ]\Theta; \Delta \vdash \subst{\varphi}{P}{\psi}。归纳假设给出 Γ⊢f:Π(P:Sort 0). φ∗\Gamma \vdash f : \tPi{P}{\Sort{0}}{\varphi^\ast}。由于 ψ\psi 的每个命题变量都在 Θ\Theta 中，从而在 Γ\Gamma 中有假设 Q:Sort 0Q : \Sort{0}，引理 A.3 给出 Γ⊢ψ∗:Sort 0\Gamma \vdash \psi^\ast : \Sort{0}。T-App 给出

Γ⊢f  ψ∗:φ∗[P↦ψ∗]=(φ[P↦ψ])∗,\Gamma \vdash f\;\psi^\ast : \subst{\varphi^\ast}{P}{\psi^\ast} = (\subst{\varphi}{P}{\psi})^\ast,

其中最后一步是上一节的替换等式。

逻辑的每条规则都已覆盖，所以定理对每棵推导成立。

证明从未用到 T-Conv：它构造的每棵类型推导都只在语法上比较类型，至多相差约束变量的名字；只有当逻辑扩展了计算，比如加入第二部分的归纳类型，转换才成为必需。

要点回顾

  • 定理的精确形式带有一个显式的命题变量列表 Θ\Theta，并对每个表示 (Θ;Δ)(\Theta; \Delta) 的上下文（顺序任意）证明结论。
  • 每个翻译后的公式都位于 Sort 0\Sort{0} 中（引理 A.3）。这在 ∀\forall 情形用到非谓词性，也正是它让 ∀\forall-elim 能用任意公式实例化量词。
  • 证明是对推导的归纳；每条逻辑规则恰好对应一条类型规则：Hyp 对应 T-Var，两条引入规则对应 T-Lam，两条消去规则对应 T-App。
  • 从未用到 T-Conv，因为这个逻辑没有计算。
上一章系统的性质下一章α 等价算法的正确性