対角線補題と Tarski の定理 | 数理論理

1 自己代入を表す式

算術言語を $L_A=\{0,S,+,\times\}$ とし、変数 $x$ の符号を $v_x$ とする。構文操作の算術化で固定した捕獲回避代入関数を $\operatorname{Sub}(e,v,n)$ と書く。第1引数が一変数式の符号であるとき、自然数 $n$ を表す数詞を第2引数により指定される自由変数へ代入した式の符号を返す。不正な符号に対する値もあらかじめ固定されている。

定義 1.1.

d(n):=\operatorname{Sub}(n,v_x,n)

と定める。 $d$ は、符号 $n$ が表す式の自由変数 $x$ へ $\bar n$ を代入した式の符号を返す全域関数である。

命題 1.2. $d$ は原始再帰的である。従って、二変数算術式 $D(x,y)$ で、任意の標準自然数 $n$ について

Q\vdash\forall y\bigl(D(\bar n,y)\leftrightarrow y=\overline{d(n)}\bigr)

を満たすものが存在する。

証明. $\operatorname{Sub}$ は原始再帰全関数であり、 $v_x$ は固定した自然数である。対角写像 $n\mapsto(n,n)$ 、定数関数 $n\mapsto v_x$ 、および $\operatorname{Sub}$ の合成によって $d$ を得るため、 $d$ は原始再帰的である。原始再帰全関数の $Q$ における強い数詞ごとの表現可能性を適用すると、表示した $D(x,y)$ が存在する。▨

論理式 $D$ と外的関数 $d$ は異なる対象である。 $D(\bar n,y)$ は対象言語の式であり、 $d(n)$ はメタ理論で計算した自然数である。上の命題が両者を標準数詞ごとに接続する。

2 対角線補題

定理 2.1 (対角線補題). $\theta(x)$ を、自由変数が高々 $x$ である任意の $L_A$ 論理式とする。このとき、ある $L_A$ 文 $\psi$ が存在して

Q\vdash\psi\leftrightarrow\theta(\ulcorner\psi\urcorner)

が成り立つ。従って、 $Q\subseteq T$ を満たす任意の $L_A$ 理論 $T$ についても

T\vdash\psi\leftrightarrow\theta(\ulcorner\psi\urcorner)

である。

証明方針は、入力された式の符号を直接同じ式へ入れることではない。まず、入力 $x$ を自己代入した結果 $d(x)$ を $\theta$ へ渡す補助式を作る。次に、補助式自身の符号を補助式へ代入する。

証明.命題 1.2の式 $D(x,y)$ を用いて

\beta(x):=\exists y\bigl(D(x,y)\land\theta(y)\bigr)

と定める。 $b=\ulcorner\beta\urcorner$ とし、文

\psi:=\beta(\bar b)

を取る。Gödel 符号の定義により

d(b)=\operatorname{Sub}(b,v_x,b)=\ulcorner\beta(\bar b)\urcorner =\ulcorner\psi\urcorner

\text{(2.1.1)}

である。

$d$ の強い表現可能性から

Q\vdash\forall y\bigl(D(\bar b,y)\leftrightarrow y=\overline{d(b)}\bigr)

\text{(2.1.2)}

を得る。式 (2.1.2)と等号に関する置換可能性を用いると、 $Q$ の内部で

\begin{aligned} \psi &\leftrightarrow \beta(\bar b)\\ &\leftrightarrow \exists y\bigl(D(\bar b,y)\land\theta(y)\bigr)\\ &\leftrightarrow \theta(\overline{d(b)}) \end{aligned}

を証明することができる。式 (2.1.1)により $\overline{d(b)}$ は文 $\psi$ の Gödel 数を表す数詞である。従って

Q\vdash\psi\leftrightarrow\theta(\ulcorner\psi\urcorner)

となる。 $Q\subseteq T$ ならば、同じ有限証明は $T$ の証明でもある。▨

注意 2.2 (固定点の意味). 対角線補題では、文 $\psi$ と式 $\theta(x)$ が同じ記号列であるとは述べられない。結論は、 $\psi$ と $\theta(\ulcorner\psi\urcorner)$ の同値を $Q$ が証明するという対象理論内の主張である。また、補題の証明は $\theta$ の真偽や、理論 $T$ の無矛盾性を仮定しない。

例 2.3. $\theta(x)$ を $x=x$ とする。対角線補題により得られる文 $\psi$ は

Q\vdash\psi\leftrightarrow \ulcorner\psi\urcorner=\ulcorner\psi\urcorner

を満たす。右辺は等号公理から証明されるため、 $Q\vdash\psi$ である。この例では、 $x$ が式中に現れること自体ではなく、自己代入の構成が任意の一変数式に一様に適用されることを確認することができる。

3 標準モデルの真理を定義することはできない

算術文全体の集合を $\operatorname{Sent}(L_A)$ とする。メタ理論では

\operatorname{True}_{\mathbb N} =\{\ulcorner\sigma\urcorner:\sigma\in\operatorname{Sent}(L_A),\ \mathbb N\models\sigma\}

という自然数の集合を考えることができる。問題は、この集合の所属関係を一つの算術式 $\operatorname{Tr}(x)$ によって標準モデル内部で定義することができるかどうかである。

定理 3.1 (Tarski の真理定義不能性定理). 自由変数が高々 $x$ である $L_A$ 論理式 $\operatorname{Tr}(x)$ で、任意の $L_A$ 文 $\sigma$ について

\mathbb N\models\operatorname{Tr}(\ulcorner\sigma\urcorner) \quad\Longleftrightarrow\quad \mathbb N\models\sigma

\text{(3.1.1)}

を満たすものは存在しない。

証明方針は、 $\operatorname{Tr}$ が定義する真理を否定する一変数式へ対角線補題を適用することである。得られる文について、対角線補題により真理と $\operatorname{Tr}$ の否定が同値になり、仮定式 (3.1.1)により真理と $\operatorname{Tr}$ が同値になる。

証明.式 (3.1.1)を満たす式 $\operatorname{Tr}(x)$ が存在すると仮定する。 $\theta(x):=\neg\operatorname{Tr}(x)$ へ定理 2.1を適用し、

Q\vdash\psi\leftrightarrow \neg\operatorname{Tr}(\ulcorner\psi\urcorner)

\text{(3.1.2)}

を満たす文 $\psi$ を取る。標準モデルは $Q$ のモデルであるから、健全性により

\mathbb N\models\psi \quad\Longleftrightarrow\quad \mathbb N\not\models\operatorname{Tr}(\ulcorner\psi\urcorner)

\text{(3.1.3)}

である。一方、式 (3.1.1)を $\sigma=\psi$ に適用すると

\mathbb N\models\operatorname{Tr}(\ulcorner\psi\urcorner) \quad\Longleftrightarrow\quad \mathbb N\models\psi

\text{(3.1.4)}

を得る。式 (3.1.3)と式 (3.1.4)から、命題 $\mathbb N\models\psi$ が自身の否定と同値であることが得られるため矛盾する。従って、式 (3.1.1)を満たす算術式は存在しない。▨

注意 3.2 (Tarski の定理の量化範囲). 定理で否定されるのは、標準モデルにおけるすべての $L_A$ 文の真理を一様に定義する算術式である。定理では特定の理論 $T$ を仮定せず、 $T$ の無矛盾性も仮定しない。定理集合 $\{\ulcorner\sigma\urcorner:T\vdash\sigma\}$ の定義可能性や列挙可能性は、標準モデルの真理集合とは別の問題である。

4 メタ言語と対象言語の区別

次の四つは異なる種類の記述である。

$d(n)=m$ は、自然数を入力とする外的計算についての等式である。
$D(\bar n,\bar m)$ は、外的計算を表す対象言語の文である。
$Q\vdash D(\bar n,\bar m)$ は、その算術文に対する形式的証明の存在である。
$\mathbb N\models D(\bar n,\bar m)$ は、その算術文の標準モデルにおける真理である。

対角線補題では、項目 (1)から項目 (2)へ表現可能性によって移り、項目 (2)について項目 (3)の同値を構成する。Tarski の定理では、項目 (3)で得た同値を $\mathbb N\models Q$ によって項目 (4)へ移し、仮定した真理定義と比較する。どの段階でも、メタ言語の自己参照を前提にはしていない。

5 演習

問題 5.1. 次の問いに答えよ。

対角線補題の証明で、 $\beta(x)$ を単に $\theta(x)$ とせず、 $D(x,y)$ を介して定義する理由を述べよ。
Tarski の定理の証明で、 $\mathbb N\models Q$ を用いる箇所を特定せよ。
Tarski の定理へ理論 $T$ の無矛盾性を追加する必要がない理由を述べよ。

解答 (確認問題の解答).

(1)では、 $x$ を式の入力として用いるだけでなく、その入力が表す式へ同じ入力を代入した符号 $d(x)$ を $\theta$ へ渡す必要があることを述べる。(2)では、 $Q$ 内で証明した固定点同値式 (3.1.2)を標準モデルで真な同値式 (3.1.3)へ移す段階を挙げる。(3)では、矛盾が標準モデルにおける真理定義式 (3.1.1)と固定点同値から直接生じ、任意の追加理論の証明可能性を用いていないことを述べればよい。▨

§E16.22対角線補題と Tarski の定理

1 自己代入を表す式

2 対角線補題

3 標準モデルの真理を定義することはできない

4 メタ言語と対象言語の区別

5 演習

参考文献

前提記事