假设判断与一般判断

假设判断

假设判断 表示一个或多个假设和一个结论之间的蕴含关系。举个简单的假设判断的例子——「人被杀就会死」。其中「人被杀」是假设，「（人）就会死」是结论。其中有两个重要的概念，称为 可推导性 和 可接受性。

可推导性

给定一个规则的集合 $ R $，和一些判断 $ J_1,…,J_k $，我们将规则集 $ R $ 与这些判断生成的公理

$$ \frac{}{J_1} \quad … \quad \frac{}{J_k} $$

的并集表示为 $ R[J_1,…,J_k] $，称为规则集的 扩展。如果从这个扩展的集合中能够推导出判断 $ K $，则记为 $ J_1,…,J_k \vdash_{R} K $。其中我们将假设 $ J_1,…,J_k $ 作为一种「临时公理」，与规则集 $ R $ 一起推导出结论 $ K $。此时称判断 $ K $ 是可推导的。

一般使用大写的希腊字母 $ \Gamma $ 或 $ \Delta $ 表示有限的判断集合，如设 $ \Gamma $ 为 $ J_1,…,J_k $，上面的式子就可以简写为 $ R[\Gamma] $ 和 $ \Gamma \vdash_{R} K $。另外也可以使用 $ \vdash_{R} \Gamma $ 表示对于每个 $ \Gamma $ 中的判断 $ J $，$ \vdash_{R} J $ 都成立。

$ J_1,…,J_n \vdash_{R} J $ 的另一种说法是，规则

$$ \frac{J_1 ~ … ~ J_n}{J} \tag{3.1} $$

可以通过 $ R $ 推导得出。

使用前一章的规则 $ (2.2) $ 举个例子

$$ a ~ \text{nat} \vdash_{(2.2)} succ(succ(a)) ~ \text{nat} \tag{3.2} $$

定理 3.1（稳定性）. 如果 $ \Gamma \vdash_{R} J $，那么 $ \Gamma \vdash_{R \cup R’} J $。

因为 $ R $ 中的规则都存在于 $ R \cup R’ $ 中，因此这条定理是显而易见的。同样地还具备以下性质：

自反性. $ \Gamma,J \vdash_{R} J $. 任何假设可以推导出自身作为结论。

弱化性. 如果 $ \Gamma \vdash_{R} J $，那么 $ \Gamma,K \vdash_{R} J $. 多余的扩展不会影响结论，这条与稳定性定理类似。

可传递性. 如果 $ \Gamma,K \vdash_{R} J $ 且 $ \Gamma \vdash_{R} K $，那么 $ \Gamma \vdash_{R} J $. 这条也可以通过规则推导定理得到。

可接受性

可接受性 同样表示规则和判断之间的关系。$ \Gamma \vDash_{R} J $ 表示当所有假设 $ \Gamma $ 都能由规则集 $ R $ 推导时，$ J $ 也能由 $ R $ 推导出来。

$$ succ(a) ~ \text{nat} \vDash_{(2.2)} a ~ \text{nat} \tag{3.6} $$

这条判断是成立的，因为根据 $ (2.2b) $，可以通过反向查询得出，如果 $ succ(a) ~ \text{nat} $ 必然有 $ a ~ \text{nat} $。

可接受性与可推导性具有高度相似的性质：

自反性. $ \Gamma,J \vDash_{R} J $.

弱化性. 如果 $ \Gamma \vDash_{R} J $，那么 $ \Gamma,K \vDash_{R} J $.

可传递性. 如果 $ \Gamma,K \vDash_{R} J $ 且 $ \Gamma \vDash_{R} K $，那么 $ \Gamma \vDash_{R} J $.

定理 3.2. 如果 $ \Gamma \vdash_{R} J $，那么 $ \Gamma \vDash_{R} J $。

证明： 根据可推导性的传递性可以得到，如果 $ \Gamma \vdash_{R} J $ 且 $ \vdash_{R} \Gamma $，则 $ \vdash_{R} J $。符合可接受性的定义。

也就是说，如果一条判断是可推导的，那它必然也是可接受的。

假设归纳定义

我们可以在归纳定义中的假设和结论中使用可推导性的判断。这里可以引出两个概念：局部假设 和 全局假设。其中局部假设只对特定的前提有效，而全局假设对所有的前提和结论都有效。一个 假设归纳定义 由一组 假设规则 组成，具有以下形式：

$$ \frac{\Gamma ~ \Gamma_1 \vdash J_1 ~ … ~ \Gamma ~ \Gamma_n \vdash J_n}{\Gamma \vdash J} \tag{3.9} $$

假设 $ \Gamma $ 为全局假设，$ \Gamma_i $ 为第 $ i $ 个前提的局部假设。这条规则的含义为，如果所有 $ J_i $ 可以被 $ \Gamma~\Gamma_i $ 导出，那么 $ J $ 也可以被 $ \Gamma $ 导出。在很多情况下，全局规则会在上下文中给出，此时可以省略全局规则写为

$$ \frac{\Gamma_1 \vdash J_1 ~ … ~ \Gamma_n \vdash J_n}{J} \tag{3.10} $$

形式化的可推导性判断 $ \Gamma \vdash J $ 由一个基本判断的有限集 $ \Gamma $ 与一个基本判断组成。假设规则集 $ R $ 表示满足以下规则的强闭合规则集合：

$$ \frac{}{\Gamma,J \vdash J} \tag{3.11a} $$

$$ \frac{\Gamma \vdash J}{\Gamma,K \vdash J} \tag{3.11b} $$

$$ \frac{\Gamma \vdash K \quad \Gamma,K \vdash J}{\Gamma \vdash J} \tag{3.11c} $$

假设归纳定义是普通归纳定义加上假设判断的扩展，因此与之前类似，如果想证明性质 $ P(\Gamma \vdash J) $ 对于任意 $ \Gamma \vdash J $ 成立，我们需要证明：如果任意 $ P(\Gamma~\Gamma_i \vdash J_i) $ 成立，那么 $ P(\Gamma \vdash J) $。

一般判断

一般判断用来表示包含变量的判断。在一般的数学理论中，变量是一个特定集合中未知的对象。一个 一般的 判断表示一个判断对于变量的任意取值都成立。另外一般判断中还包含对参数的处理。我们用 $ \Gamma \vdash_{R}^{U:X} J $ 表示在规则集 $ R $ 以及绑定的参数 $ U $ 和变量 $ X $ 的情况下，$ \Gamma $ 可以推导出 $ J $。一般可推导性可以被定义为：

$$ \vec{x} \mid \Gamma \vdash_{R}^{X} J \iff \forall\pi:\vec{x} \leftrightarrow \vec{x}’\pi\cdot\Gamma \vdash_{R}^{X,\vec{x}’} \pi\cdot J $$

即对于任意的重命名 $ \pi:\vec{x} \leftrightarrow \vec{x}’ $，$ \Gamma $ 都可以推导出 $ J $。以下的一般推导

$$ \frac{\frac{\frac{}{x ~ \text{nat}}}{succ(x) ~ \text{nat}}}{succ(succ(x)) ~ \text{nat}} $$

可以用于证明判断

$$ x \mid x ~ \text{nat} \vdash_{(2.2)}^{X} succ(succ(x)) ~ \text{nat} $$

一般可推导性判断具备以下性质

扩散性. 如果 $ \vec{x} \mid \Gamma \vdash_{R}^{X} J $，那么 $ \vec{x},x \mid \Gamma \vdash_{R}^{X} J $。多余的变量不影响结果。

重命名. 如果 $ \vec{x},x \mid \Gamma \vdash_{R}^{X} J $，那么 $ \vec{x},x \mid [x \leftrightarrow x’] \cdot \Gamma \vdash_{R}^{X} [x \leftrightarrow x’] J $ 对于任意 $ x’ \notin X,\vec{x}’ $ 成立。

变量应用. 如果 $ \vec{x},x \mid \Gamma \vdash_{R}^{X} J $ 且 $ a \in B[X,\vec{x}] $，那么 $ \vec{x} \mid [a/x] \Gamma \vdash_{R}^{X} [a/x] J $。变量可以应用为实际的值。

参数化的可推导性和变量类似：

$$ \vec{u};\vec{x} \mid \Gamma \vdash_{R}^{U;X} J \iff \forall\rho:\vec{u}\leftrightarrow\vec{u}’ ~ \forall\pi:\vec{x} \leftrightarrow \vec{x}’ \rho\cdot\pi\cdot\Gamma \vdash_{R}^{U,\vec{u}’;X,\vec{x}’} \rho\cdot\pi\cdot J $$

一般归纳定义

一般归纳定义 在普通的假设归纳定义的基础上扩展了变量的使用，一条一般规则具有以下形式：

$$ \frac{\vec{x}\vec{x_1} \mid \Gamma ~ \Gamma_1 \vdash J_1 ~ … ~ \vec{x}\vec{x_n} \mid \Gamma ~ \Gamma_n \vdash J_n}{\vec{x} \mid \Gamma \vdash J} \tag{3.12} $$

类似地，$ \vec{x} $ 是规则中的 全局变量，而 $ \vec{x_i} $ 是每个前提的 局部变量。全局变量也可以被省略，记为

$$ \frac{\vec{x_1} \mid \Gamma_1 \vdash J_1 ~ … ~ \vec{x_n} \mid \Gamma_n \vdash J_n}{J} \tag{3.13} $$

为了保证一般判断符合推导规则，需要满足：

$$ \frac
{}
{\vec{x} \mid \Gamma,J \vdash J}
\tag{3.14a} $$

$$ \frac
{\vec{x} \mid \Gamma \vdash J}
{\vec{x} \mid \Gamma,J’ \vdash J}
\tag{3.14b} $$

$$ \frac
{\vec{x} \mid \Gamma \vdash J}
{\vec{x},x \mid \Gamma \vdash J}
\tag{3.14c} $$

$$ \frac
{\vec{x},x’ \mid [x \leftrightarrow x’] \cdot \Gamma \vdash [x \leftrightarrow x’] \cdot J}
{\vec{x},x \mid \Gamma \vdash J}
\tag{3.14d} $$

$$ \frac
{\vec{x} \mid \Gamma \vdash J \quad \vec{x} \mid \Gamma,J \vdash J’}
{\vec{x},x \mid \Gamma \vdash J’}
\tag{3.14e} $$

$$ \frac
{\vec{x},x \mid \Gamma \vdash J \quad a \in B[\vec{x}]}
{\vec{x} \mid [a/x] \Gamma \vdash [a/x]J}
\tag{3.14f}
$$

总结

这部分介绍了假设判断和一般判断，将前面提到的规则扩展到了更加复杂的形式。规则中可以包含更加复杂的逻辑判断，并且可以处理变量和参数。假设判断中的可推导性和可接受性表达了逻辑中的蕴含关系。这两个性质有很多相似的地方，暂时没有找到合适的形象的例子来区分二者。但是总得来说可推导性比可接受性更加“严格”一些。

终于整完第一部分了，写公式太麻烦了，弃坑之。。