7.1. KP 的自增强

KP 的自增强并不按我们之前引入的 Levy 对句子复杂度的分层来.

定义 7.1.0.1. 我们考虑以下两类公式.

1.	如果 $\phi$ 是无量词公式 $\psi$ 前面附加有穷多个受限量词和存在量词所得, 则称它是一个 $\Sigma$ 公式.
2.	如果 $\phi$ 是无量词公式 $\psi$ 前面附加有穷多个受限量词和任意量词所得, 则称它是一个 $\Pi$ 公式.
3.	如果理论 $T$ 可证 $\phi$ 同时等价于一个 $\Sigma$ 公式和一个 $\Pi$ 公式, 则称 $\phi$ 是一个 ${\Delta }^T$ 公式.

显然, 它和 Levy 层级的区别在于: $\forall x\in y\exists z(\psi )$ 是 $\Sigma$ 公式, 但它作为 $\forall x\exists z(x\in y\to \psi )$ 是 ${\Pi }_2$ 公式.

$KP$ 的自增强主要围绕 $\Sigma$ 公式展开.

元定理 7.1.0.2 (弱 $\Sigma$ 反射公理模式). 任给 $\Sigma$ 公式 $\phi$, $KP⊢\phi \leftrightarrow \exists c({\phi }^c)$.

评注. 注意, 完整的反射公理模式要求 $c$ 传递.

证明. 我们对 $\phi$ 的复杂度归纳. 显然 ${\Delta }_0$ 的句子对任何传递集绝对, 且 $\Sigma$ 句子都向上绝对, 因此我们只需证明 $\phi \to \exists c({\phi }^c)$; 首先来对所有无量词公式证明此事.

1.	原子公式及原子公式的否定显然任取 $c$ 都可以.
2.	若已有 ${\phi }_1\to \exists c_1({\phi }_1^{c_1})$ 和 ${\phi }_2\to \exists c_2({\phi }_1^{c_2})$, 令 $c=c_1\cup c_2$ 即得 $({\phi }_1\wedge {\phi }_2)\to \exists c({\phi }_1^c\wedge {\phi }_2^c)$.
3.	$\vee$ 完全同上造就.

评注. 我们这里把否定全部丢到原子公式上面来避免讨论 $\neg \phi$.

接下来往上面加量词, 显然只需考虑存在量词和受限任意量词两种情况; 假定已有 $\phi \to \exists c({\phi }^c)$, $x$ 在 $\phi$ 中自由出现.

1.	我们来想办法证明 $\exists x(\phi )\to \exists d\exists x\in d({\phi }^d)$. 显然只要令 $d=c\cup x$.
2.	我们来想办法证明 $\forall x\in y(\phi )\to \exists d\forall x\in y({\phi }^d)$. 由假设有 $\forall x\in y(\phi \to \exists c({\phi }^c))$ 也就是 $\forall x\in y(\phi )\to \forall x\in y\exists c({\phi }^c)$, 又鉴于 ${\phi }^c$ 显然 ${\Delta }_0$, 由 ${\Delta }_0$ 局部收集公理模式就得到 $\exists e\forall x\in y\exists c\in e({\phi }^c)$, 令 $d=\bigcup e$ 即可.

$\square$

元定理 7.1.0.3. $KP$ 可证: 任何 $\Sigma$ 公式都等价于某个 ${\Sigma }_1$ 公式.

证明. 这是因为 $\exists c({\phi }^c)$ 是 ${\Sigma }_1$ 的, 而根据弱 $\Sigma$ 反射公理模式它与 $\Sigma$ 公式 $\phi$ 等价.

$\square$

元定理 7.1.0.4 ($\Sigma$ 局部收集公理模式). 任给 $\Sigma$ 公式 $\phi$, $KP⊢(LColl{)}_{\phi }$.

证明. 假定 $\forall x\in a\exists y(\phi )$, 对整个句子用弱 $\Sigma$ 反射公理模式得到 $\exists c\forall x\in a\exists y\in c({\phi }^c)$, 用 ${\Delta }_0$ 分离公理模式得到 $b=\{y\in c|\exists x\in a({\phi }^c)\}$, 于是 $\forall x\in a\exists y\in b({\phi }^c)$, 又鉴于 ${\phi }^c\to \phi$ 最终有 $\forall x\in a\exists y\in b(\phi )$.

$\square$

元定理 7.1.0.5 (${\Delta }^{KP}$ 分离公理模式). 任给 ${\Delta }^{KP}$ 公式 $\phi$, $KP⊢(Sep{)}_{\phi }$.

证明. 假定 $\phi$ 和 $\Sigma$ 句子 ${\phi }_{\sigma }$、$\Pi$ 句子 ${\phi }_{\pi }$ 均 $KP$ 可证等价, 则把 $\phi$ 的排中律改写一下就有 $\forall x({\phi }_{\sigma }\vee \neg {\phi }_{\pi })$. 现在指定一个 $a$, 我们来分离 $b=\{x\in a|\phi \}$. 注意到 $\forall x\in a({\phi }_{\sigma }\vee \neg {\phi }_{\pi })$ 是 $\Sigma$ 句子, 于是可以用弱 $\Sigma$ 反射公理模式得到 $\exists c\forall x\in a({\phi }_{\sigma }^c\vee \neg {\phi }_{\pi }^c)$. 现在 ${\phi }_{\sigma }^c$ 是 ${\Delta }_0$ 公式, 我们用 ${\Delta }_0$ 分离公理模式取出 $b=\{x\in a|{\phi }_{\sigma }^c\}$. 绝对性指出 ${\phi }_{\sigma }^c\to {\phi }_{\sigma }$, 因此 $b$ 包含于所要的那个的 $b$; 另一方面, 如果 $x\in a$ 满足 $\phi$, 则它也满足 ${\phi }_{\pi }$, 绝对性说它满足 ${\phi }_{\pi }^c$, 而 ${\phi }_{\sigma }^c\vee \neg {\phi }_{\pi }^c$, 因此有 ${\phi }_{\sigma }^c$, 这就说明这个 $b$ 确实是我们想要的 $b$.

$\square$

元定理 7.1.0.6 ($\Sigma$ 替代公理模式). 任给 $\Sigma$ 公式 $\phi$, $KP⊢(Rep{)}_{\phi }$.

证明. 先用 $\Sigma$ 收集, 然后用 ${\Delta }^{KP}$ 分离.

$\square$

评注. 只要有卡氏积公理和 ${\Delta }_0$ 分离公理模式, 替代公理模式中指出的是这个关系所给的像集还是这个关系所给的函数都一样.

元定理 7.1.0.7 ($\Sigma$ 强替代公理模式). 任给 $\Sigma$ 公式 $\phi$, $KP⊢(SRep{)}_{\phi }$.

证明. 我们先用 $\Sigma$ 收集和 ${\Delta }^{KP}$ 造出 $f$ 像集的并, 然后弱 $\Sigma$ 反射, 于是对每个 $x\in a$ 由 ${\Delta }_0$ 分离有一个确定的 $f(a)$ 为其子集, 用 $\Sigma$ 替代即可.

$\square$

接下来, 我们讨论归纳与递归的相关问题. 由于 $\Sigma$ 公式一定被 $KP$ 认为是 ${\Sigma }_1$ 公式, 而它自己有 ${\Pi }_1$ 基础公理模式, 我们可以对 $\Sigma$ 公式随意使用 $\in$ 归纳法, 因此我们只要讨论递归定义. 我们首先考虑最重要的递归定义的函数: 传递闭包.

元定理 7.1.0.8. $KP⊢(TCl)$.

证明. 定义 $Q(x,a)$ 为 $x\subseteq a\wedge \mathrm{isTrans}(a)\wedge \forall b(x\subseteq b\wedge \mathrm{isTrans}(b)\to a\subseteq b)$, 这描述了 $a$ 作为 $\mathrm{TCl}(x)$ 应有的性质. 这句话 ${\Pi }_1$, 且显然 $Q(x,a)\wedge Q(x,b)\to a=b$.

我们现在换过来定义 $P(x,a)$ 为 $$\begin{gathered} x\subseteq a\wedge \mathrm{isTrans}(a)\wedge \forall z\in a\exists f\exists n(\mathrm{isFun} \\ (f)\wedge \mathrm{isNat}(n)\wedge \exists i\in n\wedge \mathrm{dom}(f)=\mathrm{Succ}(n)\wedge z=f(\varnothing )\wedge x=f(n)\wedge \forall i\in n(f(i)\in f(\mathrm{Succ}(i)))) \end{gathered}$$, 这描述了 $a=\mathrm{TCl}(x)=x\cup (\cup x)\cup (\cup \cup x)\cup ...$ 这一性质. 这句话 ${\Sigma }_1$.

我们证明 $P(x,a)\to Q(x,a)$. 假定 $x\subseteq b\wedge \mathrm{isTrans}(b)$, 我们证明 $a\subseteq b$ 即 $\forall z\in a(z\in b)$. 这是因为假定 $f,n$ 见证 $z\in a$, 我们证明 $\forall i\in n(f(i)\in b)$, 进而 $z=f(\varnothing )\in b$. 如若不然, 运用集合基础公理可选出最大反例 $i$ 使得 $f(i)\notin b$ 但全体让 $i\in j\in n$ 的 $j$ 都让 $f(j)\in b$; 我们再次宣称此时 $\forall j(i\in j\in n\to f(j)\subseteq b)$, 否则运用集合基础公理可选出最小的反例 $j$ 使得 $f(j)$ 不是 $b$ 子集但 $f(\mathrm{Succ}(j))\subseteq b$, 但 $f(j)$ 是前者的元素而 $b$ 传递, 矛盾; 有了这个断言后我们就知道 $f(i)\in f(\mathrm{Succ}(i))\subseteq b$ 再次矛盾, 于是证毕.

上个断言的显然推论是 $P(x,a)\wedge P(x,b)\to a=b$. 我们现在证明 $\forall x\exists a(P(x,a))$, 这按刚才的论证就导出 $(TCl)$. 鉴于 $\exists a(P(x,a))$ 是 $\Sigma$ 句子, 我们使用 $\in$ 归纳法. $x=\varnothing$ 无需多言, 因此我们获得前提 $\forall y\in x\exists b(P(y,b))$. 又鉴于 $\mathrm{TCl}(x)=x\cup {\bigcup }_{y\in x}\mathrm{TCl}(y)$, 我们就证完了.

$\square$

推论 7.1.0.9. $\mathrm{TCl}$ 是 ${\Delta }^{KP}$ 函数符号.

我们先把 $\Sigma$ 公式的 $\in$ 归纳法换成更易于处理的形式.

元定理 7.1.0.10 ($\Sigma$ 公式的 $\mathrm{TCl}$ 归纳法). 任给 $\Sigma$ 公式 $\phi (x,...)$ 我们都有 $\forall x((\forall y\in \mathrm{TCl}(x)(\phi (y)))\to \phi (x))\to \forall x(\phi (x))$.

证明. 我们用 $\in$ 归纳法证明 $\forall x\forall y\in \mathrm{TCl}(x)(\phi (y))$. 注意 $\forall y\in \mathrm{TCl}(x)(\phi (y))$ 是 $\exists t(t=\mathrm{TCl}(x)\wedge \forall y\in t(\phi (y)))$, 鉴于 $\mathrm{TCl}$ 是 ${\Delta }^{KP}$ 也是 $\Sigma$ 的我们知道这句话确实是 $\Sigma$ 的从而确可归纳. 余下工作其实显然.

$\square$

评注. $\mathrm{TCl}$ 归纳法之于 $\in$ 归纳法, 正如第二数学归纳法之于数学归纳法.

元定理 7.1.0.11 ($\Sigma$ 递归定义原理). 取 $\mathfrak{n}+2$ 元 $\Sigma$ 公式定义的 $KP$ 可证函数符号 $G$, 按以下方案定义的 $F$ 同样由 $\Sigma$ 公式被 $KP$ 可证为函数符号:$$F(v_0,...,v_{\mathfrak{n}-1},x)=G(v_0,...,v_{\mathfrak{n}-1},x,F\upharpoonright \mathrm{TCl}(x))$$

证明. 显然, $y=F(...,x)$ 会被定义为 $\exists f\exists d(d=\mathrm{TCl}(x)\wedge \mathrm{isFun}(f)\wedge d=\mathrm{dom}(f)\wedge \forall w\in d(f(w)=G(...,w,f\upharpoonright \mathrm{TCl}(w)))\wedge z=G(...,x,f))$, 这当然 $\Sigma$, 于是我们要证明的是 $\forall v...\forall x\exists !y(y=F(...,x))$. 余下的证明无非是照搬 $ZF$ 中完整版本的证明, 并在合适的地方以 $\mathrm{TCl}$ 归纳法代替原本完整的归纳法.

$\square$

我们立即欢乐得知:

推论 7.1.0.12. $KP\supseteq PROV$, $KPI\supseteq LPROV$.