logic 设计

logic 包把内核的等式演算转化为命题逻辑。它将联结词定义为内核定义，从十条原始规则推导出自然演绎规则，并维护证明脚本可以引用的定理名称目录。本页给出这些定义，推导这些规则，并解释该包为何无需被信任即可完成这一切。

设计目标

内核只认识等词和选择。用户则希望使用 $\top$ 、 $\bot$ 、 $\wedge$ 、 $\Rightarrow$ 、 $\neg$ 和 $\vee$ 及其常规规则。目标是在不引入任何新权限的前提下提供它们：每个联结词都是经 DefOK 闸门接纳的定义，每条规则都是调用内核规则的 MoonBit 函数。该包可能出错，表现为无法证明某些命题，但它不可能证明任何假命题。

数学背景

作为定义的联结词

QED 沿用 HOL Light 的定义，其中每个联结词都归约为等词。¹1 J. Harrison，HOL Light Tutorial，关于逻辑常量的章节；这些定义可追溯到 Andrews 的类型论 Q0。QED 的析取与 HOL Light 不同，见下文。设 $t$ 为真值项 $(\lambda x.\,x) = (\lambda x.\,x)$ 。前奏 (prelude) 定义了

\begin{aligned} \top &:= t \\ \bot &:= (\lambda p.\,p) = (\lambda p.\,t) \\ \mathit{and} &:= \lambda p\,q.\;(\lambda f.\,f\,p\,q) = (\lambda f.\,f\,t\,t) \\ \mathit{imp} &:= \lambda p\,q.\;\mathit{and}'\,p\,q = p \\ \mathit{not} &:= \lambda p.\;\mathit{imp}'\,p\,\bot' \\ \mathit{or} &:= \lambda p\,q.\;\mathit{imp}'\,(\mathit{not}'\,p)\,q \end{aligned}

其中带撇的名称表示已展开的定义体，使每个右端都是仅基于 $=$ 的闭项。各定义的含义如下：

$t$ 为真，因为它是 REFL 的一个实例。
$\bot$ 表示布尔上的恒等谓词等于恒真谓词，即 $\forall p.\,p$ ，其中 $\forall P := (P = \lambda x.\,t)$ 。它在标准模型中为假，因为否则 $\bot$ 自身就必须为真。
$p \wedge q$ 表示序对 $(p, q)$ 无法被任何函数 $f$ 与 $(t, t)$ 区分，这恰好在 $p$ 和 $q$ 都为真时成立。
$p \Rightarrow q$ 即 $(p \wedge q) = p$ ：把 $q$ 加到 $p$ 上不会改变任何东西。
$\neg p$ 即 $p \Rightarrow \bot$ 。
$p \vee q$ 即 $\neg p \Rightarrow q$ 。

基础项

prop_mk_and 及其同类函数返回的是基础形式，即展开后的右端，而不是常量的应用 $\mathit{and}\,p\,q$ 。下面的规则作用于基础形式，因为只有基础形式才能被内核规则直接处理；这些常量的存在，是为了记录定义、可被引用，并能在用户编写的项中被识别。

设计决策

推导，而非假设

该包的每条规则都是一个推导。下面的推导就是代码所执行的推导；每一行都是一条内核规则。

真。由定义 $\vdash \top = t$ ，对称性给出 $\vdash t = \top$ ，而 $\vdash t$ 即 REFL，因此 EQ_MP 给出 $\vdash \top$ （logic_prop_truth_const_thm）。对称性本身也是推导出来的：

\begin{aligned} &\vdash (=) = (=) && \textsf{REFL} \\ &\Gamma \vdash (=)\,s = (=)\,t && \textsf{MK\_COMB}(\cdot,\ \Gamma \vdash s = t) \\ &\Gamma \vdash (s = s) = (t = s) && \textsf{MK\_COMB}(\cdot,\ \vdash s = s) \\ &\Gamma \vdash t = s && \textsf{EQ\_MP}(\cdot,\ \vdash s = s) \end{aligned}

从证明到与真值的等式。 由 $\Gamma \vdash p$ 和 $\vdash t$ ，DEDUCT_ANTISYM_RULE 给出 $\Gamma \setminus \{t\} \vdash p = t$ ，并且除非 $t$ 本身是假设，否则 $\Gamma \setminus \{t\} = \Gamma$ ；若 $t$ 是假设，丢弃它也无妨，因为 $t$ 可证。这个“EQT_INTRO”步骤就是命题被放入项中的方式。

合取引入。 由 $\Gamma \vdash p$ 和 $\Delta \vdash q$ 得到 $\Gamma \vdash p = t$ 和 $\Delta \vdash q = t$ 。对于新变量 $f$ ，

\begin{aligned} &\vdash f = f && \textsf{REFL} \\ &\Gamma \vdash f\,p = f\,t && \textsf{MK\_COMB} \\ &\Gamma \cup \Delta \vdash f\,p\,q = f\,t\,t && \textsf{MK\_COMB} \\ &\Gamma \cup \Delta \vdash (\lambda f.\,f\,p\,q) = (\lambda f.\,f\,t\,t) && \textsf{ABS},\ f \notin \mathrm{FV}(\Gamma \cup \Delta) \end{aligned}

最后一行就是 $p \wedge q$ 。 $f$ 是新变量，这使得 ABS 可以适用。

合取消去。 用 MK_COMB 和 REFL 把 $\Gamma \vdash (\lambda f.\,f\,p\,q) = (\lambda f.\,f\,t\,t)$ 的两边应用到选择子 $\lambda x\,y.\,x$ 上，再用 BETA 和 TRANS 归约两边：

\Gamma \vdash (\lambda x\,y.\,x)\,p\,q = (\lambda x\,y.\,x)\,t\,t \quad\leadsto\quad \Gamma \vdash p = t

对称性以及带 $\vdash t$ 的 EQ_MP 给出 $\Gamma \vdash p$ 。选择子 $\lambda x\,y.\,y$ 则给出 $q$ 。

蕴含消去。 由 $\Gamma \vdash (p \wedge q) = p$ 和 $\Delta \vdash p$ ：对称性给出 $\Gamma \vdash p = (p \wedge q)$ ，EQ_MP 给出 $\Gamma \cup \Delta \vdash p \wedge q$ ，再由合取消去得到 $q$ 。

蕴含引入。 由 $\Gamma \vdash q$ 且 $p \in \Gamma$ ：用 $\{p\} \vdash p$ 做合取引入，得到 $\Gamma \vdash p \wedge q$ ，再从该假设做消去，得到 $\{p \wedge q\} \vdash p$ 。然后

\frac{\Gamma \vdash p \wedge q \qquad \{p \wedge q\} \vdash p}{(\Gamma \setminus \{p\}) \cup (\{p \wedge q\} \setminus \{p \wedge q\}) \vdash (p \wedge q) = p}\;\textsf{DEDUCT\_ANTISYM\_RULE}

假设集合为 $\Gamma \setminus \{p\}$ 。结论按定义即 $p \Rightarrow q$ 。logic_prop_imp_intro_thm 要求 $p \in \Gamma$ ；解除一个不存在的假设需要先做弱化。

爆炸原理 (ex falso)。 由 $\Gamma \vdash (\lambda p.\,p) = (\lambda p.\,t)$ 和任意命题 $q$ ，用 MK_COMB 配合 $\vdash q = q$ 以及两步 BETA，得到 $\Gamma \vdash q = t$ ，从而得到 $\Gamma \vdash q$ 。否定消去就是结论为 $\bot$ 的蕴含消去。

析取引入。 由 $\Gamma \vdash p$ ：假设 $\neg p$ ，将其与 $p$ 消去得到 $\bot$ ，由爆炸原理推出 $q$ ，再解除 $\neg p$ ：

\Gamma \vdash \neg p \Rightarrow q \;=\; p \vee q.

由 $\Delta \vdash q$ ，右引入在把未使用的 $\neg p$ 与 $q$ 合取之后将其解除。

没有析取消去

前奏把 $p \vee q$ 定义为 $\neg p \Rightarrow q$ 。如上所示，引入是可推导的。消去，即由 $p \vee q$ 、 $p \Rightarrow r$ 和 $q \Rightarrow r$ 推出 $r$ ，则不可推导：它需要对 $p$ 做情形分析，也就是排中律 $p \vee \neg p$ 。在 HOL 中，排中律可由选择公理和外延性推出（Diaconescu 定理），²2 R. Diaconescu，“Axiom of choice and complementation”，Proc. AMS 51，1975。HOL Light 在 class.ml 中以这种方式推导 EXCLUDED_MIDDLE。但内核没有暴露选择公理的定理，该包也不推导排中律。与其提供一条无法证成的规则，目录中只有 or_intro_l 和 or_intro_r 而没有 or_elim，策略层有 left 和 right 而没有情形分析。

对联结词常量的可信识别

问题。 用户可以声明一个名为 and 但含义不同的常量。如果 prop_dest_and 识别任何名为 and 的常量的应用，策略就可能把任意项当作合取。

选择。 析构函数接受基础形式（按结构检查），而仅当状态中持有该常量的规范定义定理（且标识为当前标识）时，才接受联结词常量的应用。install_prop_prelude 拒绝在名称和类型都正确但没有定义的占位常量之上安装。

原因。 识别错误不会破坏可靠性，因为每条规则都经内核重放。但它们会在重放时产生令人困惑的失败，而不是在策略处给出清晰的失败；而规范要求联结词识别必须有定义支撑。

一个目录，两种模式

问题。 exact th 和 apply th 含义不同。exact 需要结论即目标的定理；apply 需要后件即目标的蕴含，并把其前件留作新目标。若允许名称被悄悄用于错误的模式，要么晚失败，要么更糟：让 exact 悄悄表现得像 apply。

选择。 每个目录条目记录 exact_class 和 apply_class。exact 只查询前者，apply 只查询后者；存在但在某种模式下不可用的名称解析为 KnownButUnavailable，策略层将其报告为形状或 apply 不匹配。局部假设名称始终优先于目录名称，且绝不回退到目录名称。

原因。 该表是策略层、证明器语料 (corpus)、映射矩阵和文档的唯一来源，因此用户可以书写的定理名称不会在它们之间漂移。

错误仅来自内核

内核错误构造子在内核之外是只读的。该包通过运行已知会以所需方式失败的小型内核操作，来获得它所返回的 LogicError 和 SigError 值。这使错误词汇由内核掌握，代价是错误不够具体：许多辅助函数的失败会表现为 TypeMismatch 或 AlphaMismatch。

正确性与不变量

可靠性。 该包返回的每个 Thm 都是内核函数的结果，因此内核的可靠性论证覆盖了它。上面的推导表明，每条规则对其预期用途也是完备的：只要前提具有所述形状，它就会成功。
前奏的保守性。 这六个常量通过 DefOK 接纳，右端为闭项，不含类型变量，也无环，因此前奏是空理论的保守扩张。
幂等性。 install_prop_prelude(install_prop_prelude(s)) 等于 install_prop_prelude(s)：已存在的规范定义按原样接受。
精确的相继式。 重放辅助函数按 α 等价检查作为集合的假设。logic_prop_strengthen_to_hyps 只会增加假设，因此需要目标所没有的假设的定理会被拒绝，而不是带着额外假设被接受。
β 规范化会产生证明。 logic_beta_normalize_eq 和 logic_normalize_prop_beta 逐步构造内核等式；项层面的 logic_beta_nf_* 函数返回这类等式的右端。规范化不进入抽象，并且有界（每轮 512 步，深层形式 32 轮），这足以满足联结词编码。

被否决的替代方案

将联结词作为内核原语。 这会给内核及其可靠性证明增加规则。而定义在信任上没有任何代价。
HOL Light 的析取 $\forall r.\,(p \Rightarrow r) \Rightarrow (q \Rightarrow r) \Rightarrow r$ 。使用它时，无需排中律即可推导消去，代价是每个析取内部都要对命题做全称量化。前奏使用更短的编码并明确声明其限制；改用前者会改变每个析取项以及建立在其上的语料。
混合解析器。 logic_prop_resolve_ref 解析名称时不区分模式；保留它是为了测试，而策略层使用按模式区分的解析器。

边界

该包只证明命题事实；除策略层为定理头部绑定子构建的规则外，它没有量词规则。
它没有析取消去、排中律，也没有经典推理。
它不存储用户定理：目录固定在源码中，添加名称意味着添加代码和测试。
它不增加任何权限。对它的任何修改都是审查其有用性，而非可靠性。
它不解析或打印公式；项由 parser 构建，由内核的结构化打印器打印。

J. Harrison，HOL Light Tutorial，关于逻辑常量的章节；这些定义可追溯到 Andrews 的类型论 Q0。QED 的析取与 HOL Light 不同，见下文。 ↩
R. Diaconescu，“Axiom of choice and complementation”，Proc. AMS 51，1975。HOL Light 在 class.ml 中以这种方式推导 EXCLUDED_MIDDLE。 ↩