Craigの絡繰とその相対化

数理論理学,Craigの絡繰,再帰理論

通報

再帰的可算な理論と初等再帰的な理論が一致するというCraigの絡繰 (Craig's trick) とその算術的階層への一般化を紹介する。以下では言語に指数関数に対する関数記号が含まれていると仮定する。

算術的階層

$\Delta^0_0$ を有界論理式全体の集合とする。
$\Sigma^0_0:=\Pi^0_0:=\Delta^0_0$ とする。
$\Sigma^0_{n+1}$ を、ある $\varphi(x)\in\Pi^0_n$ に対して $\exists x\varphi(x)$ と表せる論理式の集合とする。
$\Pi^0_{n+1}$ を、ある $\varphi(x)\in\Sigma^0_n$ に対して $\forall x\varphi(x)$ と表せる論理式の集合とする。

定義可能性

集合$X\subseteq\mathbb{N}^\nu$が$\Gamma$-定義可能 ($\Gamma$-definable) であるとは、ある$\varphi\in\Gamma$ が存在し$X=\{\vec{x}\in\mathbb{N}^\nu\mid\mathbb{N}\models\varphi(\vec{x})\}$となることである。
関数$f$が$\Gamma$-定義可能であるのはそのグラフが$\Gamma$-定義可能であることとし、理論$T$が$\Gamma$-定義可能であるのは$T$に含まれる論理式のコード全体$\{\ulcorner\varphi\urcorner\mid\varphi\in T\}$が$\Gamma$-定義可能であることとする。

一般化されたCraigの絡繰

任意の$\Sigma^0_{n+1}$-定義可能な理論$T$に対し、ある$\Pi^0_n$-定義可能な理論$S$が存在し、任意の論理式$\varphi$に対し$$T\vdash\varphi\Longleftrightarrow S\vdash\varphi$$となる。

まず再帰理論の基本的結果、空でない集合$X$が$\Sigma^0_{n+1}$-定義可能であることと$X$はある$\Pi^0_n$-定義可能関数の値域となることが同値になることに気をつける。今、理論$T$が空だとするど自明に成立つので空でないとし、$\Pi^0_n$-定義可能な関数$f$で$\mathrm{rng}(f)=\{\ulcorner\varphi\urcorner\mid\varphi\in T\}$となるようなものを取る。また論理式$\varphi$に対して$\varphi^n$を$\varphi^0:=\top,\varphi^{n+1}:=\varphi^n\land\varphi$と定めて、理論$S$を$S:=\{\varphi^{n+1}\mid f(n)=\ulcorner\varphi\urcorner\}$とする。$S$の定義から$$T\vdash\varphi\Longleftrightarrow S\vdash\varphi$$となることは明らか。また$n$と$\ulcorner\varphi\urcorner$から$\ulcorner\varphi^n\urcorner$を返す関数、すなわち$g(n,\ulcorner\varphi\urcorner)=\ulcorner\varphi^n\urcorner$を満たす関数$g$は初等再帰的であることから$x\in\{\ulcorner\varphi\urcorner\mid\varphi\in S\}$は$(\exists y< x)[x=g(y+1,f(y))]$と同値であり、$\Pi^0_n$-定義可能である。