対角化補題

同義語：不動点補題diagonal lemmadiagonalization lemmafixed-point lemma

概要

前提知識: 一階述語論理, Gödel数化, 計算可能関数

「この文は証明できない」「この文は真でない」のように、文が自分自身について語ることを、算術の言語の中で正確に実現するのが 対角化補題（diagonal lemma、不動点補題 ともいう）である。主張は次のとおり。自由変数が $y$ だけの任意の論理式 $\psi(y)$ に対して、文 $\sigma$ で
$$ \mathsf Q\vdash\sigma\leftrightarrow\psi(\ulcorner\sigma\urcorner) $$
となるものがある。ここで $\mathsf Q$ は足し算と掛け算についてのごく弱い公理系、$\ulcorner\sigma\urcorner$ は $\sigma$ の Gödel 数を表す数項である。$\sigma$ は「私は性質 $\psi$ をもつ」と述べる文で、しかもその言い分が $\mathsf Q$ の中で証明できる形で正しい。$\psi$ を「証明できない」にとれば Gödelの不完全性定理の証明に、「真でない」にとれば Tarskiの真理定義の記事の Tarski の真理の定義不可能性定理に、「証明できるならば $\varphi$」にとれば Löbの定理になる。
Gödel数化の記事の番号付けでは、文が自分の番号を記号列としてそのまま含むことはできない（ex-dl-counterexamples の 3 行目）。補題が与えるのは、記号列としての一致ではなく、$\mathsf Q$ で証明できる同値である。

設定

算術の言語を $L_A=\{0,S,+,\cdot,<\}$、その標準的な構造を $\mathfrak N=(\mathbb N,0,S,+,\cdot,<)$（$S$ は $n\mapsto n+1$）とする。$n\in\mathbb N$ の数項 $\underline n$ は $0$ に $S$ を $n$ 個付けた項 $S\cdots S0$ で、その値はどの割り当てでも $n$ である。$L_A$ の文の集合を理論とよび、$T\vdash\varphi$ は $T$ から $\varphi$ が一階述語論理で導出できることを表す。
Robinson の算術 $\mathsf Q$ は、$S$ の単射性 $\forall x\forall y\,(Sx=Sy\to x=y)$、$\forall x\,\lnot(0=Sx)$、$\forall x\,(\lnot x=0\to\exists y\,x=Sy)$、和と積の再帰の式 $x+0=x$、$x+Sy=S(x+y)$、$x\cdot0=0$、$x\cdot Sy=x\cdot y+x$（それぞれ全称閉包をとる）、および $<$ の定義 $\forall x\forall y\,\bigl(x< y\leftrightarrow\exists z\,(Sz+x=y)\bigr)$ の 8 個の文からなる理論である（Gödelの不完全性定理の記事の定義「Robinson の算術と Peano 算術」、Robinson算術の定義「Robinson算術」と同じ）。$\mathfrak N$ は $\mathsf Q$ のモデルである。理論 $T$ が $\mathsf Q$ の 8 個の公理をすべて導出するとき、$T$ は $\mathsf Q$ を含む という。
項と論理式の Gödel 数は Gödel数化の記事の定義「項と論理式の Gödel 数」で固定し、論理式 $\varphi$ の Gödel 数を $\#\varphi$、その数項を $\ulcorner\varphi\urcorner:=\underline{\#\varphi}$ と書く。変数 $x:=v_0$、$y:=v_1$ を固定する。

関数の表現と対角化関数

関数 $f\colon\mathbb N\to\mathbb N$ が理論 $T$ で 表現可能 であるとは、自由変数が $x,y$ の中にある論理式 $F(x,y)$ があって、すべての $n\in\mathbb N$ について
$$ T\vdash F(\underline n,\underline{f(n)}),\qquad T\vdash\forall y\,\bigl(F(\underline n,y)\to y=\underline{f(n)}\bigr) $$
となることをいう。このとき $F$ は $f$ を $T$ で 表現する という。
対角化関数 $d\colon\mathbb N\to\mathbb N$ を、$n=\#\theta$ で、$\theta$ が論理式であり $\theta$ に自由に現れる変数が $x$ だけ（またはない）とき $d(n):=\#\theta(\underline n)$、それ以外のとき $d(n):=0$ と定める。ここで $\theta(\underline n)$ は $\theta$ の自由な $x$ をすべて $\underline n$ に置き換えた文である。

$d(\#\theta)$ は、$\theta$ に自分自身の Gödel 数の数項を入れた文 $\theta(\ulcorner\theta\urcorner)$ の Gödel 数である。この「自分の番号を自分に入れる」操作を $\theta$ の 対角化 とよぶ。$d$ は原始再帰関数である（Gödel数化の記事の定理「対角化関数は原始再帰的」）。

この記事では証明しない事実

計算可能な関数はすべて $\mathsf Q$ で表現可能である（OLT26 Theorem 35.27、p. 566。逆も成り立つことを含めた形が Theorem 35.2、p. 553）。とくに $d$ は $\mathsf Q$ で表現可能であり、$\mathsf Q$ を含む理論 $T$ でも同じ論理式が $d$ を表現する。

対角化補題

$T$ を、対角化関数 $d$ が表現可能な理論とする（rem-dl-facts により、$\mathsf Q$ を含む理論はすべてそうである）。自由変数が $y$ の中にある任意の論理式 $\psi(y)$ に対して、文 $\sigma$ で
$$ T\vdash\sigma\leftrightarrow\psi(\ulcorner\sigma\urcorner) $$
を満たすものがある。とくに、どの $\psi(y)$ にも $\mathsf Q\vdash\sigma\leftrightarrow\psi(\ulcorner\sigma\urcorner)$ となる文 $\sigma$ がある。

自分の対角化を指す式を対角化する

$D(x,y)$ を、$d$ を $T$ で表現する論理式とする。束縛変数の名前を付け替えて、$D$ の束縛変数は $y$ と異なるとしてよい。
$$ \theta(x):=\exists y\,\bigl(D(x,y)\land\psi(y)\bigr) $$
とおく。$D$ の自由変数は $x,y$ の中に、$\psi$ の自由変数は $y$ の中にあり、$y$ は量化されているので、$\theta$ に自由に現れる変数は $x$ だけ（またはない）である。$n:=\#\theta$ とし、$\theta$ を対角化した文
$$ \sigma:=\theta(\underline n)=\exists y\,\bigl(D(\underline n,y)\land\psi(y)\bigr) $$
をとる。$d$ の定義により $d(n)=\#\sigma$、すなわち $\underline{d(n)}=\ulcorner\sigma\urcorner$ である。$D$ が $d$ を表現することから、次の (1)・(2) が成り立つ。

1. $T\vdash D(\underline n,\ulcorner\sigma\urcorner)$
1. $T\vdash\forall y\,\bigl(D(\underline n,y)\to y=\ulcorner\sigma\urcorner\bigr)$
  $T$ の中で $\sigma\leftrightarrow\psi(\ulcorner\sigma\urcorner)$ を導く。
  （$\to$）$\sigma$ を仮定し、$D(\underline n,y)\land\psi(y)$ を満たす $y$ をとる。(2) により $y=\ulcorner\sigma\urcorner$ なので、等号の規則により $\psi(\ulcorner\sigma\urcorner)$ が成り立つ。存在記号の除去により $\sigma\to\psi(\ulcorner\sigma\urcorner)$ が導出できる。
  （$\leftarrow$）$\psi(\ulcorner\sigma\urcorner)$ を仮定すると、(1) と合わせて $D(\underline n,\ulcorner\sigma\urcorner)\land\psi(\ulcorner\sigma\urcorner)$ が成り立ち、存在記号の導入により $\exists y\,\bigl(D(\underline n,y)\land\psi(y)\bigr)$、すなわち $\sigma$ が成り立つ。
  使ったのは一階述語論理の規則と (1)・(2) だけなので、$T\vdash\sigma\leftrightarrow\psi(\ulcorner\sigma\urcorner)$ である。$\square$

同じ補題は OLT26 Lemma 37.1（p. 581。$\mathsf Q$ を含む理論について）・Lemma 37.2（p. 583。$\mathsf Q$ について）にあり、証明の考え方は同書 §37.2（pp. 581–583）で説明されている。集合論 ZF の言語と理論での同じ形は Kun80 Chapter I, Theorem 14.2（p. 40）にある。

直感

構成の鍵は、$\theta(x)$ が「$x$ を番号にもつ論理式を対角化した文は性質 $\psi$ をもつ」と読めることである。$\theta$ を、自分自身の番号を入れて対角化すると、できた文 $\sigma$ は「$\theta$ を対角化した文は性質 $\psi$ をもつ」と述べる。ところが $\theta$ を対角化した文とは $\sigma$ 自身である。こうして $\sigma$ は、自分の名前を直接書き込むことなく、「自分を作る手順」を書き込むことで自分を指す。
日常語に移すと、「『を引用符に入れて前に付けると、性質 $\psi$ をもつ文になる』を引用符に入れて前に付けると、性質 $\psi$ をもつ文になる」という文がこの構成にあたる。文は引用された句について語っているだけだが、句に指示どおりの操作をすると文そのものになる。同じ考え方は Cantorの対角線論法の「表の対角成分を変える」操作や、プログラムが自分の番号を参照してよいことを保証する Kleeneの再帰定理にも現れる。

例

Gödel 文と嘘つきの文

$T$ を $\mathsf Q$ を含む決定可能な公理系とし、「$y$ は $T$ から導出できる論理式の番号である」を表す論理式 $\mathrm{Prov}_T(y)$ を Gödelの不完全性定理の記事の節「証明できることを算術の文で表す」のようにとる。thm-dl-main を $\psi:=\lnot\mathrm{Prov}_T$ に使うと、$\mathsf Q\vdash G_T\leftrightarrow\lnot\mathrm{Prov}_T(\ulcorner G_T\urcorner)$ となる文 $G_T$（Gödel 文）が得られ、$T$ が無矛盾なら $T\not\vdash G_T$ である（同記事の定理「Gödel 文の性質」）。$\psi$ を「真な文の番号の集合を定義する式」の否定にとれば嘘つきの文になり、そのような式が存在しないことが Tarski の定理である（Tarskiの真理定義の記事の定理「Tarski の真理の定義不可能性定理」）。

不動点はただ 1 つではない

$\psi(y):=(y=y)$ とする。$\psi(\ulcorner\sigma\urcorner)$ は $\ulcorner\sigma\urcorner=\ulcorner\sigma\urcorner$ で論理的に正しいので、$\mathsf Q\vdash\sigma\leftrightarrow\psi(\ulcorner\sigma\urcorner)$ は $\mathsf Q\vdash\sigma$ と同値である。したがって $\psi$ の不動点は、ちょうど $\mathsf Q$ から導出できる文であり、$0=0$ も $\lnot(0=S0)$ もそうである。この 2 つは記号列として異なる。一般に thm-dl-main が与える $\sigma$ は 1 つの構成の産物であって、性質 $\psi$ だけから決まる文ではない。

1 元の構造の理論

$E=\{e\}$ を、すべての記号を $e$ で解釈した（$<^E=\emptyset$ とする）$L_A$ 構造とし、$T_E:=\{\varphi:\varphi\text{ は文で }E\models\varphi\}$ とする。$E$ では変数を含まない項の値はすべて $e$ なので、論理式 $D(x,y):=(y=y)$ は対角化関数 $d$ を $T_E$ で表現する。実際 $D(\underline n,\underline{d(n)})$ は $\underline{d(n)}=\underline{d(n)}$ なので $T_E\vdash D(\underline n,\underline{d(n)})$ であり、$E\models\forall y\,(y=\underline m)$ なので $T_E\vdash\forall y\,(D(\underline n,y)\to y=\underline{d(n)})$ である。よって thm-dl-main により、$T_E$ ではすべての $\psi(y)$ に不動点がある。直接にも、$E\models\psi[e]$ なら $\sigma:=(0=0)$、そうでなければ $\sigma:=\lnot(0=0)$ とおけば $E\models\sigma\leftrightarrow\psi(\ulcorner\sigma\urcorner)$ である。
一方 $T_E$ は無矛盾で、どの文についても文か否定を含み、決定可能な文の集合である（決定可能な理論の記事の定理「有限構造の理論は決定可能」）。したがって $T_E$ には独立な文がない。$T_E$ は $\mathsf Q$ を含まない（$E\models0=S0$）。対角化補題が成り立つだけでは不完全性は出てこず、Gödelの不完全性定理の議論には、導出の関係を正しく表す論理式が要る。$T_E$ ではすべての数項が等しいので、そのような論理式はない。

パラメータつきの形と意味論の形

不動点として文だけでなく、自由変数を残した論理式も作れる。$z_1,\dots,z_k$ を $x,y$ と異なる変数とし、$\vec z=(z_1,\dots,z_k)$ と書く。

パラメータつきの対角化補題

自由変数が $y,z_1,\dots,z_k$ の中にある任意の論理式 $\psi(y,\vec z)$ に対して、自由変数が $z_1,\dots,z_k$ の中にある論理式 $\theta(\vec z)$ で
$$ \mathsf Q\vdash\forall\vec z\,\bigl(\theta(\vec z)\leftrightarrow\psi(\ulcorner\theta\urcorner,\vec z)\bigr) $$
を満たすものがある。ここで $\ulcorner\theta\urcorner$ は、自由変数をもつ論理式 $\theta$ の Gödel 数の数項である。

要点は、prf-dl-main の $d$ を、自由変数の制限なしに $x$ へ自分の番号を代入する関数に替えて、同じ推論を $\vec z$ を自由にしたまま行うことである。

詳しい証明を開く

$d^+(n)$ を、$n$ が論理式 $\alpha$ の Gödel 数なら $\#\bigl(\alpha[\underline n/x]\bigr)$（$\alpha$ の自由な $x$ をすべて $\underline n$ に置き換えた論理式の番号）、そうでなければ $0$ と定める。Gödel数化の記事の定理「構文の関係と操作の原始再帰性」の 2（$\operatorname{Fm}$）と 6（$\operatorname{Sb}$）により、$d^+(n)$ は $\operatorname{Fm}(n)$ のとき $\operatorname{Sb}(n,0,n)$、そうでないとき $0$ という場合分けで書けるので原始再帰的であり、rem-dl-facts により $\mathsf Q$ で論理式 $D^+(x,y)$ によって表現される。束縛変数を付け替えて、$D^+$ の束縛変数は $y,z_1,\dots,z_k$ と異なるとする。

$\alpha(x,\vec z):=\exists y\,\bigl(D^+(x,y)\land\psi(y,\vec z)\bigr)$、$m:=\#\alpha$、$\theta(\vec z):=\alpha[\underline m/x]=\exists y\,\bigl(D^+(\underline m,y)\land\psi(y,\vec z)\bigr)$ とおく。$\theta$ の自由変数は $z_1,\dots,z_k$ の中にあり、$d^+(m)=\#\theta$ である。表現の定義から $\mathsf Q\vdash D^+(\underline m,\ulcorner\theta\urcorner)$ と $\mathsf Q\vdash\forall y\,\bigl(D^+(\underline m,y)\to y=\ulcorner\theta\urcorner\bigr)$ が成り立つ。

あとは prf-dl-main の（$\to$）（$\leftarrow$）と同じ推論を、$\vec z$ を自由変数のまま行うと $\mathsf Q\vdash\theta(\vec z)\leftrightarrow\psi(\ulcorner\theta\urcorner,\vec z)$ を得る。$\mathsf Q$ の公理は文なので、全称記号の導入により $\mathsf Q\vdash\forall\vec z\,\bigl(\theta(\vec z)\leftrightarrow\psi(\ulcorner\theta\urcorner,\vec z)\bigr)$ である。$\square$

自分の番号だけを定義する論理式

thm-dl-param を $k=1$、$\psi(y,z_1):=(z_1=y)$ に使うと、自由変数が $z_1$ の中にある論理式 $\theta(z_1)$ で $\mathsf Q\vdash\forall z_1\,\bigl(\theta(z_1)\leftrightarrow z_1=\ulcorner\theta\urcorner\bigr)$ となるものがある。$\mathfrak N$ は $\mathsf Q$ のモデルなので、健全性により $\mathfrak N$ で $\theta$ が定義する集合はちょうど $\{\#\theta\}$ である。$\theta$ は「私が満たす数は、私の番号だけである」と述べる論理式で、自分自身を出力するプログラムの論理式版にあたる。

$\mathfrak N$ での真偽に移した形は次のとおりである。thm-dl-main の $\sigma$ について、健全性により $\mathfrak N\models\sigma\leftrightarrow\psi(\ulcorner\sigma\urcorner)$ であり、数項 $\ulcorner\sigma\urcorner$ の値は $\#\sigma$ なので、一階述語論理の記事の補題「代入補題」により
$$ \mathfrak N\models\sigma\iff\mathfrak N\models\psi[\#\sigma] $$
（右辺は $y$ に $\#\sigma$ を割り当てる）が成り立つ。$d$ のグラフを $\mathfrak N$ で定義する論理式を使って同じ文を直接作る証明が、Tarskiの真理定義の記事の補題「対角化補題（意味論の形）」である。

応用：真理を理論の中で定義できないこと

対角化補題から直ちに従う典型的な帰結として、真理の定義不可能性の構文の形を示す。

真理述語は無矛盾な理論の中にない

$T$ を $\mathsf Q$ を含む無矛盾な理論とする。自由変数が $y$ の中にある論理式 $\mathrm{Tr}(y)$ で、すべての文 $\sigma$ について
$$ T\vdash\sigma\leftrightarrow\mathrm{Tr}(\ulcorner\sigma\urcorner) $$
となるものは存在しない。

嘘つきの文を作る

そのような $\mathrm{Tr}$ があったとする。thm-dl-main を $\psi:=\lnot\mathrm{Tr}$ に使い、$T\vdash\lambda\leftrightarrow\lnot\mathrm{Tr}(\ulcorner\lambda\urcorner)$ となる文 $\lambda$ をとる。$\mathrm{Tr}$ の性質から $T\vdash\lambda\leftrightarrow\mathrm{Tr}(\ulcorner\lambda\urcorner)$ でもあるので、命題論理により $T\vdash\lambda\leftrightarrow\lnot\lambda$ である。$(\lambda\leftrightarrow\lnot\lambda)\to\lnot\lambda$ と $(\lambda\leftrightarrow\lnot\lambda)\to\lambda$ はともに恒真式なので、$T\vdash\lnot\lambda$ かつ $T\vdash\lambda$ となり、$T$ の無矛盾性に反する。$\square$

$\lambda$ は「私は（$\mathrm{Tr}$ の意味で）真でない」と述べる文である。$T$ が $\mathfrak N$ をモデルにもつとき、cor-dl-truth は「$\mathfrak N$ の真理を $T$ が証明できる形で定める式はない」と読める。$\mathfrak N$ での定義可能性についての、より強い形が Tarski の定理である（Tarskiの真理定義の記事の定理「Tarski の真理の定義不可能性定理」）。この形は OLT26 Problem 37.1（p. 594）の主張にあたる。
対角化補題は、ほかにも次の定理の証明の出発点になる。

$\psi(y)$ にとる性質	得られる文	帰結
導出できない $\lnot\mathrm{Prov}_T(y)$	Gödel 文	第1不完全性定理（Gödelの不完全性定理）
真でない（$\mathfrak N$ での形）	嘘つきの文	Tarski の真理の定義不可能性定理（Tarskiの真理定義）
「それより短い反証がない証明がある」の否定	Rosser 文	無矛盾性だけを仮定した第1不完全性定理（OLT26 Theorem 37.7、p. 585）
導出できるならば $\varphi$：$\mathrm{Prov}_T(y)\to\varphi$	Löb の証明の文	Löbの定理

反例：条件を外すと成り立たない

外す条件	反例	成り立たなくなること
cor-dl-truth の「無矛盾」	$L_A$ のすべての文の集合 $T_{\mathrm{all}}$	真理述語 $\mathrm{Tr}$ が存在しないこと
cor-dl-truth の「すべての文」	量化記号を含まない文だけに制限する（$T=\mathsf Q$）	真理述語 $\mathrm{Tr}$ が存在しないこと
thm-dl-main の結論の「$T$ で証明できる同値」（記号列の一致を求める）	$y$ が自由に現れる任意の $\psi(y)$	条件を満たす文 $\sigma$ が存在すること

反例の確かめ

1 行目：$T_{\mathrm{all}}$ は $\mathsf Q$ を含み、どの文も導出するので、$\mathrm{Tr}(y):=(y=y)$ について $T_{\mathrm{all}}\vdash\sigma\leftrightarrow\mathrm{Tr}(\ulcorner\sigma\urcorner)$ がすべての文 $\sigma$ で成り立つ。
2 行目：量化記号を含まない文の全体を $\mathrm{QF}$ とし、そのうち $\mathfrak N$ で真なものの Gödel 数の集合を $Z$ とする。$Z$ に属すかどうかは、変数を含まない項の値を足し算と掛け算で計算し、等号・大小と結合子の真偽を調べればアルゴリズムで判定できるので、Church–Turingのテーゼにより $Z$ は計算可能である。

2 行目の残りの確かめを開く

計算可能な関係は $\mathsf Q$ で表現可能なので（OLT26 Theorem 35.29、p. 567）、論理式 $\theta_0(y)$ で、$\#\sigma\in Z$ なら $\mathsf Q\vdash\theta_0(\ulcorner\sigma\urcorner)$、$\#\sigma\notin Z$ なら $\mathsf Q\vdash\lnot\theta_0(\ulcorner\sigma\urcorner)$ となるものがある。一方、量化記号を含まない文は有界な量化だけでできた文の特別な場合なので、$\mathfrak N$ で真なものはすべて $\mathsf Q$ から導出できる（OLT26 Lemma 35.37、p. 570）。$\sigma\in\mathrm{QF}$ が真なら $\mathsf Q\vdash\sigma$ と $\mathsf Q\vdash\theta_0(\ulcorner\sigma\urcorner)$ から、偽なら真な文 $\lnot\sigma\in\mathrm{QF}$ について $\mathsf Q\vdash\lnot\sigma$ と $\mathsf Q\vdash\lnot\theta_0(\ulcorner\sigma\urcorner)$ から、どちらの場合も $\mathsf Q\vdash\sigma\leftrightarrow\theta_0(\ulcorner\sigma\urcorner)$ である。prf-dl-truth の論法を $\theta_0$ に使っても、対角化で作る文 $\lambda$ は量化記号 $\exists y$ を含み $\mathrm{QF}$ の外にあるので、矛盾は生じない。

3 行目：$\sigma=\psi(\ulcorner\sigma\urcorner)$ が記号列として成り立つ文 $\sigma$ はない。

3 行目の確かめを開く

そのような $\sigma$ があったとする。$y$ は $\psi$ に自由に現れるので、項 $\ulcorner\sigma\urcorner=\underline{\#\sigma}$ は $\sigma$ の部分項として現れる。Gödel数化の記事の補題「成分は符号より小さい」の 1 をくり返し使うと、論理式 $\sigma$ に部分として現れる項の Gödel 数は $\#\sigma$ より小さいので、$\#\underline{\#\sigma}<\#\sigma$ である。他方、同記事の数項の符号 $\operatorname{num}$ は $\operatorname{num}(0)=4$、$\operatorname{num}(m+1)=\langle2,\operatorname{num}(m)\rangle$ を満たし、同じ補題の 1 により $\operatorname{num}(m+1)>\operatorname{num}(m)$ なので、帰納法により $\operatorname{num}(m)\ge m+4>m$ である。$m:=\#\sigma$ とおくと $\#\underline{\#\sigma}=\operatorname{num}(\#\sigma)>\#\sigma$ となり、矛盾する。

3 行目が示すように、自己言及は記号列の上の循環ではなく、理論の中で証明できる同値として実現される。これが「この文」という言い回しを数学的に正当化する仕組みである。

補足

集合論への移植：$\mathsf Q$ の代わりに ZF を使っても、$d$ を表現する論理式を作れば同じ証明が通る。Kun80 Chapter I, Theorem 14.2（p. 40）は ZF での形を述べ、同 Theorem 14.3（p. 41）でそれを ZF の拡大の第2不完全性定理に使う。
計算論との対応：Kleeneの再帰定理は、文の代わりにプログラムの番号について同じ形の不動点を与える（OLT26 p. 583 の注意）。