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

1 自己代入を表す式

算術言語を $L_A=\{0,S,+,\times\}$ とし、変数 $x$ の符号を $v_x$ とする。構文操作の算術化で固定した捕獲回避代入関数を $\operatorname{Sub}(e,v,n)$ と書く。 $\operatorname{Sub}$ は、第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 Tarski の真理定義不能性定理

算術文全体の集合を $\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)の段階の対象言語の文を得る。次に、その文について項目 (3)の段階の同値を構成する。Tarski の定理の証明では、項目 (3)の段階で得た同値から、 $\mathbb N\models Q$ を用いて項目 (4)の段階の同値を導き、仮定した真理定義と比較する。どの段階でも、メタ言語の自己参照を前提にはしていない。

5 演習

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

自由変数が高々 $x$ である $L_A$ 論理式 $\theta(x)$ を固定する。 $Q\vdash\psi\leftrightarrow\theta(\ulcorner\psi\urcorner)$ を満たす文 $\psi$ で、互いに異なるものが無限個存在することを示せ。
$M$ を $Q$ の任意のモデルとする。自由変数が高々 $x$ である $L_A$ 論理式 $\operatorname{Tr}(x)$ で、任意の $L_A$ 文 $\sigma$ について $M\models\operatorname{Tr}(\ulcorner\sigma\urcorner)$ と $M\models\sigma$ が同値になるものは存在しないことを示せ。
$T$ を $Q\subseteq T$ を満たす $L_A$ 理論とする。 $T$ が構文的に無矛盾ならば、任意の $L_A$ 文 $\sigma$ について $T\vdash\operatorname{Tr}(\ulcorner\sigma\urcorner)\leftrightarrow\sigma$ を満たす論理式 $\operatorname{Tr}(x)$ は存在しないことを示せ。また、 $T$ が構文的に無矛盾でないならば、そのような $\operatorname{Tr}(x)$ が存在することを示せ。

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

各標準自然数 $k$ について $\theta_k(x):=\theta(x)\land\bar k=\bar k$ とおく。 $\theta_k$ の自由変数は高々 $x$ である。定理 2.1の証明の構成を $\theta_k$ に適用し、 $\beta_k(x):=\exists y\,(D(x,y)\land\theta_k(y))$ 、 $b_k=\ulcorner\beta_k\urcorner$ 、 $\psi_k:=\beta_k(\bar b_k)$ とおくと、 $Q\vdash\psi_k\leftrightarrow\theta_k(\ulcorner\psi_k\urcorner)$ である。等号の反射律から $Q\vdash\bar k=\bar k$ であるから、 $Q\vdash\theta_k(\ulcorner\psi_k\urcorner)\leftrightarrow\theta(\ulcorner\psi_k\urcorner)$ であり、 $Q\vdash\psi_k\leftrightarrow\theta(\ulcorner\psi_k\urcorner)$ を得る。

$k\neq l$ ならば $\psi_k\neq\psi_l$ であることを示す。 $\psi_k$ は $\exists y\,(D(\bar b_k,y)\land(\theta(y)\land\bar k=\bar k))$ であり、数詞は閉項であるから $x$ への代入は部分論理式 $\bar k=\bar k$ を変えない。一意可読性により、 $\psi_k=\psi_l$ ならば構文木の同じ位置にある部分論理式 $\bar k=\bar k$ と $\bar l=\bar l$ が等しく、数詞 $S^k0$ と $S^l0$ が等しいので $k=l$ である。よって $\{\psi_k\mid k\in\N\}$ は互いに異なる無限個の固定点からなる。
そのような $\operatorname{Tr}(x)$ が存在すると仮定する。定理 2.1を $\theta(x):=\neg\operatorname{Tr}(x)$ に適用し、 $Q\vdash\psi\leftrightarrow\neg\operatorname{Tr}(\ulcorner\psi\urcorner)$ を満たす文 $\psi$ を取る。 $M\models Q$ であるから、健全性により $M\models\psi$ と $M\not\models\operatorname{Tr}(\ulcorner\psi\urcorner)$ は同値である。仮定を $\sigma=\psi$ に適用すると $M\models\operatorname{Tr}(\ulcorner\psi\urcorner)$ と $M\models\psi$ は同値である。二つを合わせると、 $M\models\psi$ が自身の否定と同値になり矛盾する。この議論は定理 3.1の証明で標準モデルを $Q$ の任意のモデルに置き換えたものであり、非標準モデルでも同じ結論が成り立つ。
$T$ を構文的に無矛盾とし、そのような $\operatorname{Tr}(x)$ が存在すると仮定する。定理 2.1を $\theta(x):=\neg\operatorname{Tr}(x)$ に適用して $T\vdash\psi\leftrightarrow\neg\operatorname{Tr}(\ulcorner\psi\urcorner)$ を満たす文 $\psi$ を取る。仮定 $T\vdash\operatorname{Tr}(\ulcorner\psi\urcorner)\leftrightarrow\psi$ と合わせると、命題論理の派生則により $T\vdash\psi\leftrightarrow\neg\psi$ である。 $T\vdash\psi\to\neg\psi$ と§E19.10 補題 2.1 (1)の恒等式 $\neg\psi\to\neg\psi$ から、場合分けの派生則 $(\psi\to\neg\psi)\to((\neg\psi\to\neg\psi)\to\neg\psi)$ により $T\vdash\neg\psi$ である。すると $T\vdash\neg\psi\to\psi$ と modus ponens により $T\vdash\psi$ であり、 $T$ は構文的に無矛盾でない。これは仮定に反する。

$T$ が構文的に無矛盾でなければ、§E19.10 補題 2.1 (5)により $T$ はすべての文を導出する。とくに $\operatorname{Tr}(x):=(x=x)$ とおくと、任意の文 $\sigma$ について $T\vdash\operatorname{Tr}(\ulcorner\sigma\urcorner)\leftrightarrow\sigma$ である。したがって、導出可能性による真理定義の不存在には $T$ の無矛盾性が必要であり、標準モデルでの真理を扱う定理 3.1とはこの点で異なる。

▨

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

1 自己代入を表す式

2 対角線補題

3 Tarski の真理定義不能性定理

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

5 演習

参考文献

前提記事