用户: Trebor/高阶逻辑规则

一套构造性高阶逻辑的规则, 它自洽 (consistent)、完备 (complete), 并且有效 (effective).

1语法

定义 1.1. 高阶逻辑的类型由如下规则归纳生成:

•	$\mathbb{N},\Omega ,1$ 是类型.
•	如果 $A,B$ 是类型, 那么 $A\times B$ 是类型.
•	如果 $A$ 是类型, 那么 $\mathcal{P}(A)$ 是类型.

定义 1.2. 一列标有类型的变量名称作语境.

本文不处理变量相关问题.

定义 1.3. 对于语境 $\Gamma$ 与类型 $A$, 定义表达式的集合, 由如下规则归纳生成. 如果 $t$ 是语境 $\Gamma$ 下 $A$ 类型的表达式, 写作 $\Gamma ⊢t:A$.

•	$\Gamma ⊢\ast :1$.
•	$\Gamma ⊢\mathsf{zero}:\mathbb{N}$.
•	如果 $\Gamma ⊢n:\mathbb{N}$, 那么 $\Gamma ⊢\mathsf{succ}(n):\mathbb{N}$.
•	如果 $\Gamma ⊢a:A$, $\Gamma ⊢b:B$, 那么 $\Gamma ⊢(a,b):A\times B$.
•	如果 $\Gamma ,x:A⊢p:\Omega$, 那么 $\Gamma ⊢\{x:A\mid p\}:\mathcal{P}(A)$.
•	如果 $\Gamma ⊢S:\mathcal{P}(A)$, $\Gamma ⊢a:A$, 那么 $\Gamma ⊢a\in S:\Omega$.
•	$\Gamma ⊢\top :\Omega$; $\Gamma ⊢\perp :\Omega$.
•	如果 $\Gamma ⊢p:\Omega$, $\Gamma ⊢q:\Omega$, 那么 $\Gamma ⊢p\wedge q:\Omega$, $\Gamma ⊢p\vee q:\Omega$, $\Gamma ⊢p\to q:\Omega$.
•	如果 $\Gamma ,x:A⊢p:\Omega$, 那么 $\Gamma ⊢(\forall x:A,p):\Omega$, $\Gamma ⊢(\exists x:A,p):\Omega$.

表达式有自然的优先级规则, 有变量代换操作, 不再写出.

2证明

如果 $\Gamma$ 下有 $\Omega$ 类型的表达式 $p,q$ (它们称作命题), 则称 $p\stackrel{\Gamma }{\Rightarrow }q$ 为相继式. 我们可以按照以下规则证明相继式.

结构规则:

•	$p\stackrel{\Gamma }{\Rightarrow }p$ 成立.
•	如果 $p\stackrel{\Gamma }{\Rightarrow }q$, $q\stackrel{\Gamma }{\Rightarrow }r$ 成立, 那么 $p\stackrel{\Gamma }{\Rightarrow }r$ 成立.

逻辑规则:

•	$\perp \stackrel{\Gamma }{\Rightarrow }q$ 与 $p\stackrel{\Gamma }{\Rightarrow }\top$ 成立.
•	$p\stackrel{\Gamma }{\Rightarrow }q\wedge r$ 成立等价于 $p\stackrel{\Gamma }{\Rightarrow }q$ 与 $p\stackrel{\Gamma }{\Rightarrow }r$ 都成立.
•	$p\vee q\stackrel{\Gamma }{\Rightarrow }r$ 成立等价于 $p\stackrel{\Gamma }{\Rightarrow }r$ 与 $q\stackrel{\Gamma }{\Rightarrow }r$ 都成立.
•	$p\wedge q\stackrel{\Gamma }{\Rightarrow }r$ 成立等价于 $p\stackrel{\Gamma }{\Rightarrow }q\to r$ 成立.
•	若 $p\stackrel{\Gamma ,x:A}{\Rightarrow }q$ 成立, 且 $p$ 不含 $x$, 则 $p\stackrel{\Gamma }{\Rightarrow }\forall x:A,q$.
•	若 $p\stackrel{\Gamma }{\Rightarrow }\forall x:A,q$ 成立且 $\Gamma ⊢t:A$, 则 $p\stackrel{\Gamma }{\Rightarrow }q[x/t]$, 其中 $q[x/t]$ 表示将 $x$ 替换为表达式 $t$.
•	若 $p\stackrel{\Gamma ,x:A}{\Rightarrow }q$ 成立, 且 $q$ 不含 $x$, 则 $\exists x:A,p\stackrel{\Gamma }{\Rightarrow }q$.
•	若 $\exists x:A,p\stackrel{\Gamma }{\Rightarrow }q$ 成立且 $\Gamma ⊢t:A$, 则 $p[x/t]\stackrel{\Gamma }{\Rightarrow }q$.

以下规定一些缩写. $p\leftrightarrow q$ 表示 $(p\to q)\wedge (q\to p)$. $\neg p$ 表示 $p\to \perp$. $s=t$ 表示 $\forall S:\mathcal{P}(A),(s\in S)\leftrightarrow (t\in S)$. 这些缩写也可以作为额外的公理加入. 这里各表达式的类型都显然, 不再写出.

非逻辑公理:

•	$\top \stackrel{\Gamma }{\Rightarrow }t\in \{y:A\mid p\}\leftrightarrow p[t/x]$.

以下公理均形如 $\top \stackrel{\Gamma }{\Rightarrow }p$, 但是 $p$ 不含任何自由变量, 因此省略前半部分.

•	$\forall x:1,x=\ast$.
•	$\forall z:A\times B,\exists x:A,\exists y:B,z=(x,y)$.
•	$\forall x:A,\forall x^{\prime }:A,\forall y:B,\forall y^{\prime }:B,(x,y)=(x^{\prime },y^{\prime })\to (x=x^{\prime }\wedge y=y^{\prime })$.
•	$\forall S:\mathcal{P}(A),\forall T:\mathcal{P}(A),(\forall x:A,x\in S\leftrightarrow x\in T)\to S=T$.
•	$\forall p:\Omega ,\forall q:\Omega ,(p\leftrightarrow q)\to (p=q)$.

Peano 公理:

•	$\forall n:\mathbb{N},\mathsf{succ}(x)=\mathsf{zero}\to \perp$.
•	$\forall m:\mathbb{N},\forall n:\mathbb{N},\mathsf{succ}(m)=\mathsf{succ}(n)\to m=n$.
•	$\forall S:\mathcal{P}(\mathbb{N}),(\mathsf{zero}\in S\wedge \forall m\in \mathbb{N},m\in S\to \mathsf{succ}(m)\in S)\to \forall n\in \mathbb{N},n\in S$.

以上规则在安排时均满足代换引理, 即使得以下规则成为元定理而无需手动加入.

引理 2.1. 如果 $p,q$ 是 $\Gamma$ 下的命题, $\sigma$ 是从 $\Delta$ 到 $\Gamma$ 的代换, 那么 $p\stackrel{\Gamma }{\Rightarrow }q$ 可以推出 $p[\sigma ]\stackrel{\Delta }{\Rightarrow }q[\sigma ]$.

证明. 反复归纳.

$\square$