Gödel数化

同義語：ゲーデル数化Gödel数ゲーデル数Gödel numberingGödel number

概要

Gödel数化（Gödel numbering）とは、記号・項・論理式・導出などの構文の対象に自然数を単射に割り当て、構文の性質や操作を自然数の上の関係や関数として扱えるようにすることであり、割り当てた数を Gödel 数という。素数冪による列の符号で項と論理式の組み立ての木を符号化すると、それまでの値をすべて参照する累積再帰によって、論理式であること、自由変数、数項の代入、自分の番号を代入する対角化関数、公理の集合が原始再帰的なときの導出の関係が、すべて原始再帰的になる。これらを算術の論理式で表すことが、Gödel の不完全性定理や Tarski の真理の定義不可能性定理の証明の出発点になる。番号付けが単射であるだけでは足りず、番号から構文を計算可能に読み戻せることが本質である。

$$\newcommand{C}[0]{\mathbb{C}} \newcommand{div}[0]{\mathbin{÷}} \newcommand{N}[0]{\mathbb{N}} \newcommand{Q}[0]{\mathbb{Q}} \newcommand{R}[0]{\mathbb{R}} \newcommand{Z}[0]{\mathbb{Z}} $$

前提知識: 原始再帰関数, 論理式, 一意可読性, 素因数分解

論理式や証明は記号を並べた有限の対象であり、自然数もまた有限の対象である。記号・項・論理式・導出のそれぞれに自然数を 1 つずつ単射に割り当て、構文についての性質や操作を自然数の上の関係や関数として扱えるようにすることを Gödel 数化（Gödel numbering）といい、割り当てた数を Gödel 数 という。構文を自然数の上の算術に移すこの方法は 構文の算術化 ともよばれ、Gödel の不完全性定理と Tarski の真理の定義不可能性定理の証明の土台になる（OLT26 §34.1、pp. 532–533）。
Gödel 数化が役に立つのは、番号を付けたうえで「$n$ は論理式の Gödel 数である」「$n$ の論理式に数項を代入した論理式の Gödel 数」「$m$ は $n$ の論理式の導出の Gödel 数である」といった関係や関数が 原始再帰関数 で書けるときである。そうなれば、算術の言語の論理式でそれらを表現でき、「この文は証明できない」と自分について語る文が作れる（Gödelの不完全性定理、Tarskiの真理定義）。この記事では、算術の言語の項と論理式に素数冪による Gödel 数を定め、構文の基本的な関係と代入・対角化の関数、さらに導出の関係が原始再帰的であることを証明する。

設定と記法

算術の言語を $L_A=\{0,S,+,\cdot,<\}$ とする（Gödelの不完全性定理 の記事の節「設定」と同じ）。変数は $v_0,v_1,v_2,\dots$、結合子は $\lnot,\land,\lor,\to$、量化記号は $\forall,\exists$ で、項と論理式は 論理式 の記事の定義「項」「論理式」による（$+,\cdot,=,<$ は中置で書く）。自然数 $m$ の 数項 $\underline m$ は、$0$ に $S$ を $m$ 個付けた項 $S\cdots S0$ である。
有限列の符号は 万能Turing機械 の記事の節「番号付け」と同じものを使う。$p(i)$ を $i$ 番目の素数（$p(0)=2$）とし、
$$ \langle a_0,\dots,a_{k-1}\rangle:=\prod_{i< k}p(i)^{a_i+1}\qquad(\langle\,\rangle=1) $$
とおく。$c\ge1$ について、$\operatorname{lh}(c)$ を $p(0),\dots,p(i-1)$ がすべて $c$ を割るような最大の $i$、$(c)_i$ を $p(i)$ が $c$ を割る最大の回数から $1$ を引いた数（$0$ 回なら $0$）とし、$\operatorname{lh}(0)=(0)_i=0$ とする。素因数分解 の一意性により、異なる列は異なる数に写り、$c=\langle a_0,\dots,a_{k-1}\rangle$ なら $\operatorname{lh}(c)=k$、$(c)_i=a_i$ である。$(i,c)\mapsto(c)_i$、$\operatorname{lh}$、列の後ろに 1 項を付け加える $\operatorname{app}(c,b):=c\cdot p(\operatorname{lh}(c))^{b+1}$ が原始再帰関数であることは、万能Turing機械 の記事の補題「列の操作は原始再帰的」で示されている。以下「原始再帰的」は 原始再帰関数 の記事の定義による。

定義

項と論理式の Gödel 数

$L_A$ の項と論理式 $E$ の Gödel 数 $\#E$ を、組み立てに沿って次で定める（$s,t$ は項、$\varphi,\psi$ は論理式）。

$E$$\#E$$E$$\#E$
$v_i$$\langle0,i\rangle$$\lnot\varphi$$\langle7,\#\varphi\rangle$
$0$$\langle1\rangle$$(\varphi\land\psi)$$\langle8,\#\varphi,\#\psi\rangle$
$St$$\langle2,\#t\rangle$$(\varphi\lor\psi)$$\langle9,\#\varphi,\#\psi\rangle$
$s+t$$\langle3,\#s,\#t\rangle$$(\varphi\to\psi)$$\langle10,\#\varphi,\#\psi\rangle$
$s\cdot t$$\langle4,\#s,\#t\rangle$$\forall v_i\,\varphi$$\langle11,i,\#\varphi\rangle$
$s=t$$\langle5,\#s,\#t\rangle$$\exists v_i\,\varphi$$\langle12,i,\#\varphi\rangle$
$s< t$$\langle6,\#s,\#t\rangle$

列の第 0 成分を 符号の種類（tag）とよぶ。種類 $0$〜$4$ が項、$5$〜$12$ が論理式である。

項と論理式は 論理式 の記事の定理「一意読み取り」により、上の規則のどれかただ 1 つで、ただ 1 通りに組み立てられるので、$\#$ は組み立てに沿った再帰で矛盾なく定まる。この記事の番号付けは、記号列を符号化する OLT26 Definition 34.1・34.3（p. 534）の方法と違い、組み立ての木をそのまま符号化している。どちらでも以下の結果は同じように成り立つが、木の符号では成分を直接読み出せるので、構文の操作が短く書ける。
導出（論理式の有限列 $\varphi_1,\dots,\varphi_k$）の Gödel 数は $\langle\#\varphi_1,\dots,\#\varphi_k\rangle$ とする。

小さな Gödel 数の計算

$\#0=\langle1\rangle=2^2=4$、$\#v_0=\langle0,0\rangle=2\cdot3=6$、$\#\underline1=\#S0=\langle2,4\rangle=2^3\cdot3^5=1944$ である。また
$$ \#(0=0)=\langle5,4,4\rangle=2^6\cdot3^5\cdot5^5=48600000,\qquad \#(v_0=0)=\langle5,6,4\rangle=2^6\cdot3^7\cdot5^5=437400000. $$
逆に $48600000$ を素因数分解すると $2^6\cdot3^5\cdot5^5$ なので、列 $\langle5,4,4\rangle$ が読み出せる。種類 $5$ は等号で、両辺の $4=2^2=\langle1\rangle$ は項 $0$ の符号だから、もとの論理式は $0=0$ である。

Gödel 数は急速に大きくなるが、大きさは問題にならない。必要なのは、番号から構文を読み戻す操作と、構文の操作に対応する番号の操作が、原始再帰関数で書けることである。

成分は符号より小さい
  1. $c=\langle a_0,\dots,a_{k-1}\rangle$ なら、すべての $i< k$ で $a_i< c$ である。
  2. $\#$ は単射である。すなわち、項または論理式 $E,E'$ について $\#E=\#E'$ なら $E=E'$ である。
  3. $v_i$ が項または論理式 $E$ に現れるなら $i<\#E$ である。

1：$p(i)^{a_i+1}$ は $c$ を割るので $c\ge p(i)^{a_i+1}\ge2^{a_i+1}>a_i$ である。
2：$E$ の組み立てについての帰納法で示す。$\#E=\#E'$ なら、素因数分解の一意性により 2 つの列は長さも成分も等しい。第 0 成分（種類）が等しいので $E$ と $E'$ は同じ規則で作られ、残りの成分も等しい。残りの成分は、変数なら添字、量化記号なら量化する変数の添字と直前の部分の Gödel 数、それ以外なら直前の部分の項・論理式の Gödel 数である。帰納法の仮定により直前の部分どうしは等しく、$E=E'$ である。
3：$v_i$ が $E$ に現れれば、$\#E$ から成分をとる操作を有限回くり返すと、$\#v_i=\langle0,i\rangle$ か、量化記号の符号 $\langle11,i,\dots\rangle$・$\langle12,i,\dots\rangle$ に至る。1 により各段で数は真に小さくなるので、至った符号は $\#E$ 以下であり、1 をもう一度使うと、どちらの場合もその成分 $i$ はその符号より小さい。よって $i<\#E$ である。$\square$

累積再帰

構文の関係は「論理式の成分が論理式である」のように、自分自身をより小さい番号で呼ぶ形で定義される。成分の番号はもとの番号より小さい（lem-gn-smaller の 1）が、1 つ前の番号とは限らない。そこで、それまでの値をすべて参照してよい再帰が原始再帰関数で閉じることを示す。
関数 $f\colon\mathbb N^{k+1}\to\mathbb N$ について、それまでの値の列の符号を
$$ \bar f(\vec x,y):=\langle f(\vec x,0),\dots,f(\vec x,y-1)\rangle\qquad(\bar f(\vec x,0)=\langle\,\rangle=1) $$
と書く。

累積再帰

$h\colon\mathbb N^{k+2}\to\mathbb N$ を原始再帰関数とする。$f\colon\mathbb N^{k+1}\to\mathbb N$ がすべての $\vec x,y$ について
$$ f(\vec x,y)=h\bigl(\vec x,y,\bar f(\vec x,y)\bigr) $$
を満たすなら、$f$ は原始再帰関数である。このような $f$ はただ 1 つである。

$F(\vec x,y):=\bar f(\vec x,y)$ とおく。$F(\vec x,y)$ は長さ $y$ の列の符号なので $\operatorname{lh}(F(\vec x,y))=y$ であり、後ろに $f(\vec x,y)$ を付け加えると $F(\vec x,y+1)$ になる。仮定の等式を代入すると
$$ F(\vec x,0)=1,\qquad F(\vec x,y+1)=\operatorname{app}\bigl(F(\vec x,y),\,h(\vec x,y,F(\vec x,y))\bigr) $$
である。$\operatorname{app}$ と $h$ は原始再帰関数なので、これは原始再帰であり、$F$ は原始再帰関数である。最後の項を読み出せば
$$ f(\vec x,y)=\bigl(F(\vec x,y+1)\bigr)_y $$
となり、$f$ も原始再帰関数である。一意性は、上の 2 式が $F$ を $y$ についての帰納法でただ 1 つに決め、$f$ が $F$ から決まることによる。$\square$

再帰の変数が最後の引数でない場合も、射影で引数を並べ替えれば同じである。関係 $R$ についても、特性関数 $\chi_R$ に lem-gn-course-of-values を使う。OLT26 §29.13（p. 439）はこの形の再帰（course-of-values recursion）を述べ、通常の原始再帰で書き直すことを読者に委ねている。上の証明がその書き直しである。

構文の関係と操作は原始再帰的

まず、自然数がどれかの列の符号であるという関係
$$ \operatorname{Seq}(c):\iff c\ge1\ \land\ c=\prod_{i<\operatorname{lh}(c)}p(i)^{(c)_i+1} $$
は、$\operatorname{lh}$・$(c)_i$・有界積が原始再帰的なので原始再帰的である（原始再帰関数 の記事の命題「有界な和・積・量化・最小化」）。以下、$\langle a,b\rangle=2^{a+1}3^{b+1}$、$\langle a,b,c\rangle=2^{a+1}3^{b+1}5^{c+1}$ も原始再帰関数である。

構文の関係と操作の原始再帰性

次の関係と関数は原始再帰的である。

  1. $\operatorname{Tm}(n)$：$n$ はある項の Gödel 数である。
  2. $\operatorname{Fm}(n)$：$n$ はある論理式の Gödel 数である。
  3. $\operatorname{Fr}(i,n)$：$n$ は項または論理式 $E$ の Gödel 数で、$v_i$ が $E$ に自由に現れる。
  4. $\operatorname{Sent}(n)$：$n$ はある文（自由変数のない論理式）の Gödel 数である。
  5. $\operatorname{num}(m):=\#\underline m$。
  6. $\operatorname{Sb}(n,i,m)$：$n=\#E$ なら $\#\bigl(E[\underline m/v_i]\bigr)$（$E$ の自由な $v_i$ をすべて $\underline m$ に置き換えたもの）、$n$ が項・論理式の Gödel 数でなければ値は何でもよい。

ここで $E[\underline m/v_i]$ は 論理式 の記事の定義「代入と代入可能性」の代入である。数項は変数を含まないので、どの論理式の $v_i$ にも代入可能である。

符号の形を調べる累積再帰

1：$\operatorname{Tm}(n)$ は次と同値である。
$$ \operatorname{Seq}(n)\land\Bigl[\bigl(\operatorname{lh}(n)=2\land(n)_0=0\bigr)\lor\bigl(\operatorname{lh}(n)=1\land(n)_0=1\bigr)\lor\bigl(\operatorname{lh}(n)=2\land(n)_0=2\land\operatorname{Tm}((n)_1)\bigr) $$
$$ \lor\bigl(\operatorname{lh}(n)=3\land((n)_0=3\lor(n)_0=4)\land\operatorname{Tm}((n)_1)\land\operatorname{Tm}((n)_2)\bigr)\Bigr]. $$
右辺で $\operatorname{Tm}$ を呼ぶ引数 $(n)_1,(n)_2$ は lem-gn-smaller の 1 により $n$ より小さい。そこで $h(n,c)$ を、右辺の $\operatorname{Tm}(j)$ を「$(c)_j=1$」に置き換えた条件の特性関数とすると、$h$ は原始再帰的な関係の論理結合の特性関数なので原始再帰関数であり、$\chi_{\operatorname{Tm}}(n)=h(n,\bar\chi_{\operatorname{Tm}}(n))$ が成り立つ。lem-gn-course-of-values により $\operatorname{Tm}$ は原始再帰的である。右辺の条件が「項の Gödel 数である」ことと同値なのは、$n$ についての累積帰納法で分かる。

同値の確かめを開く

$n=\#t$ なら、$t$ の最後の規則に応じて $n$ は右辺のどれかの形をもち、成分は部分項の Gödel 数である。逆に $n$ が右辺のどれかの形をもてば、成分 $(n)_1,(n)_2$ は $n$ より小さい項の Gödel 数（帰納法の仮定）であり、それらの項 $s,t$ から $Ss$、$s+t$ などを作ると、その Gödel 数は $n$ に等しい。変数の場合は $n=\langle0,(n)_1\rangle=\#v_{(n)_1}$、$0$ の場合は $n=\langle1\rangle$ である。


2：同じように、$\operatorname{Fm}(n)$ は $\operatorname{Seq}(n)$ と次の 4 つの場合の和の連言で書ける。種類 $5,6$ で長さ $3$、成分 $(n)_1,(n)_2$ が $\operatorname{Tm}$ を満たす。種類 $7$ で長さ $2$、$\operatorname{Fm}((n)_1)$。種類 $8,9,10$ で長さ $3$、$\operatorname{Fm}((n)_1)\land\operatorname{Fm}((n)_2)$。種類 $11,12$ で長さ $3$、$\operatorname{Fm}((n)_2)$（添字 $(n)_1$ は任意）。$\operatorname{Tm}$ はすでに原始再帰的で、$\operatorname{Fm}$ を呼ぶ引数は $n$ より小さいので、1 と同じ議論で原始再帰的である。
3：関係 $G(i,n)$ を $n$ についての累積再帰で次のように定め（$i$ はパラメータ。どの場合にも当たらない $n$ では偽）、$\operatorname{Fr}(i,n):\iff(\operatorname{Tm}(n)\lor\operatorname{Fm}(n))\land G(i,n)$ とおく。種類 $0$ なら $(n)_1=i$。種類 $1$ なら偽。種類 $2,7$ なら $G(i,(n)_1)$。種類 $3,4,5,6,8,9,10$ なら $G(i,(n)_1)\lor G(i,(n)_2)$。種類 $11,12$ なら $(n)_1\ne i\land G(i,(n)_2)$。量化記号の場合が「$\forall v_i$ の中の $v_i$ は自由でない」ことを表し、論理式 の記事の定義「自由変数と文」と一致する。
4：$\operatorname{Sent}(n)\iff\operatorname{Fm}(n)\land\forall i< n\ \lnot\operatorname{Fr}(i,n)$ である。lem-gn-smaller の 3 により、自由に現れる変数 $v_i$ はどれも $i< n$ を満たすので、有界な量化で足りる。
5：$\operatorname{num}(0)=\langle1\rangle=4$、$\operatorname{num}(m+1)=\langle2,\operatorname{num}(m)\rangle$ は原始再帰である。
6：$\operatorname{Sb}(n,i,m)$ を $n$ についての累積再帰で、種類ごとに次のように定める（$i,m$ はパラメータ、$\operatorname{Sb}$ の引数の $i,m$ は省く）。

  • 種類 $0$：$(n)_1=i$ なら $\operatorname{num}(m)$、そうでなければ $n$。種類 $1$：$n$。
  • 種類 $2,7$：$\langle(n)_0,\operatorname{Sb}((n)_1)\rangle$。種類 $3$〜$6$、$8$〜$10$：$\langle(n)_0,\operatorname{Sb}((n)_1),\operatorname{Sb}((n)_2)\rangle$。
  • 種類 $11,12$：$(n)_1=i$ なら $n$、そうでなければ $\langle(n)_0,(n)_1,\operatorname{Sb}((n)_2)\rangle$。
  • それ以外の $n$：$0$。
    場合分けの条件と各場合の式は原始再帰的で、$\operatorname{Sb}$ を呼ぶ引数は $n$ より小さいので、lem-gn-course-of-values により $\operatorname{Sb}$ は原始再帰関数である。各行は 論理式 の記事の代入の再帰（項ではすべての $v_i$ を置き換え、$\forall v_i$・$\exists v_i$ の下では置き換えない）をそのまま番号に移したものなので、項と論理式の組み立てについての帰納法で $\operatorname{Sb}(\#E,i,m)=\#(E[\underline m/v_i])$ が分かる。$\square$

対角化関数と導出の関係

不完全性定理と真理の定義不可能性定理で使う 2 つの事実、対角化関数の計算可能性と導出の関係の計算可能性を、上の定理から導く。変数 $x:=v_0$ を固定する。

対角化関数は原始再帰的

$n=\#\theta$ で $\theta$ が論理式であり、$\theta$ に自由に現れる変数が $x$ だけ（またはない）とき $d(n):=\#\theta(\underline n)$、それ以外のとき $d(n):=0$ と定める。ここで $\theta(\underline n)$ は $\theta$ の自由な $x$ をすべて $\underline n$ に置き換えた文である。このとき $d$ は原始再帰関数である。

条件「$\theta$ は論理式で、自由に現れる変数は $x=v_0$ だけ」は $\operatorname{Fm}(n)\land\forall j< n\ \bigl(\operatorname{Fr}(j,n)\to j=0\bigr)$ と同値である（lem-gn-smaller の 3 により、自由に現れる $v_j$ は $j< n$ を満たす）。この関係は thm-gn-syntax の 2・3 と有界な量化により原始再帰的である。条件が成り立つとき $d(n)=\operatorname{Sb}(n,0,n)$ であり、成り立たないとき $d(n)=0$ なので、thm-gn-syntax の 6 と場合分けにより $d$ は原始再帰関数である。$\square$

$d(\#\theta)$ は、$\theta$ に自分自身の Gödel 数の数項を入れた文の Gödel 数である。Gödelの不完全性定理 の記事の対角化関数と、Tarskiの真理定義 の記事の対角化関数（そこでは代入する変数が $v_1$）は、この $d$ と同じ形の関数であり、変数を取り替えても同じ証明が通る。両記事は、$d$ が計算可能であることを引用して使っている（Gödelの不完全性定理 の記事の注意「この記事では証明しない事実」の 2）。thm-gn-diagonal はそれを、この記事の番号付けについて証明したものである。

自分の番号について語る文

$\theta:=(v_0=0)$ とすると、ex-gn-small により $\#\theta=437400000$ であり、$\theta(\underline{\#\theta})$ は文「$\underline{437400000}=0$」である。この文は「$\theta$ の Gödel 数は $0$ である」と読め、偽である。$d(437400000)$ はこの文の Gödel 数で、$\langle5,\operatorname{num}(437400000),4\rangle$ に等しい。不完全性定理の証明では、$\theta$ として「$x$ を番号にもつ論理式に $x$ 自身を入れた文は証明できない」を表す論理式をとり、同じ操作で「私は証明できない」と語る文を作る（Gödelの不完全性定理 の記事の補題「対角化補題」）。

次に導出を扱う。一階論理の証明体系 の記事の体系 $\mathbf H$ のように、推論規則が前件肯定（MP）だけの体系を考える。論理式の集合 $\Gamma$ からの導出は、各行が論理公理か $\Gamma$ の元であるか、前の 2 行 $\psi$ と $\psi\to\chi$ から MP で得られる論理式の列である（同記事の定義「証明体系・導出・証明可能性」）。

導出の関係は原始再帰的

$A$ を論理式の集合とし、その Gödel 数の集合 $\#A:=\{\#\varphi\mid\varphi\in A\}$ は原始再帰的であるとする。関係 $\operatorname{Prf}_A(m,n)$ を「$m$ は、各行が $A$ の元であるか前の 2 行から MP で得られる論理式の列の Gödel 数で、その最後の行の Gödel 数が $n$ である」で定めると、$\operatorname{Prf}_A$ は原始再帰的である。

$\operatorname{Prf}_A(m,n)$ は次と同値である。
$$ \operatorname{Seq}(m)\land\operatorname{lh}(m)\ge1\land(m)_{\operatorname{lh}(m)\mathbin{\dot-}1}=n\land\forall k<\operatorname{lh}(m)\Bigl[(m)_k\in\#A\ \lor\ \exists i< k\ \exists j< k\ \bigl((m)_j=\langle10,(m)_i,(m)_k\rangle\bigr)\Bigr]. $$
右辺の各部分は原始再帰的な関係・関数と有界な量化からできているので、右辺は原始再帰的である。同値であることは、右辺が成り立つとき各行が論理式の Gödel 数であることを $k$ についての帰納法で確かめればよい。$(m)_k\in\#A$ なら $A$ は論理式の集合なので論理式の Gödel 数であり、$(m)_j=\langle10,(m)_i,(m)_k\rangle$ なら、$(m)_j$ は帰納法の仮定により論理式 $\psi\to\chi$ の Gödel 数で、$(m)_i=\#\psi$、$(m)_k=\#\chi$ となる。これは MP の 1 回の適用そのものである。$\square$

$T$ が論理式の集合で、$\#T$ と体系 $\mathbf H$ の論理公理の Gödel 数の集合 $\#\Lambda$ が原始再帰的なら、$A:=\Lambda\cup T$ に thm-gn-proof を使って、「$m$ は $T$ からの導出の Gödel 数で、最後の行の Gödel 数が $n$」という関係が原始再帰的になる。$\#T$ が計算可能なだけの場合も、同じ式で計算可能な関係になる（計算可能な関係が論理結合と有界な量化で閉じていることによる。この記事では証明しない）。$\#\Lambda$ が原始再帰的であること（次の rem-gn-axioms。この記事では証明しない）と合わせて、Gödelの不完全性定理 の記事の注意「この記事では証明しない事実」の 3 が得られる。

論理公理の集合

$\#\Lambda$ が原始再帰的であることは、公理図式ごとに、符号の形を調べる有界な条件で書けることから分かる。たとえば (A1) $\alpha\to(\beta\to\alpha)$ の形の論理式の Gödel 数 $n$ は
$$ (n)_0=10\land((n)_2)_0=10\land((n)_2)_2=(n)_1\land\operatorname{Fm}((n)_1)\land\operatorname{Fm}(((n)_2)_1) $$
で特徴づけられる（$\operatorname{Fm}(n)$ を合わせて課す）。代入を含む (A4) には、項の代入を表す関数と代入可能性の関係が原始再帰的であることを、thm-gn-syntax の 6 と同じ累積再帰で示して使う。全称化は先頭の量化記号を外す操作で、これも累積再帰で書ける。すべての図式についての確かめは書き下さず、$\#\Lambda$ が原始再帰的であることはこの記事では証明しない。別の公理系（公理図式・MP・量化の規則 QR）を記号列で番号付けした場合の同じ種類の主張と証明の概略が OLT26 Proposition 34.27（pp. 547–549）、そこから導出の関係が原始再帰的になることが同書 Proposition 34.28（p. 549）にある。

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

外す条件反例成り立たなくなること
lem-gn-course-of-values の「値の列は $y$ 未満」$f(y)=(\langle f(0),\dots,f(y)\rangle)_y$ の形の等式解がただ 1 つで原始再帰的であること
lem-gn-course-of-values の「$h$ は原始再帰的」$h(y,c):=\chi_K(y)$（$K$ は計算可能でない集合）$f$ が原始再帰的であること
thm-gn-syntax の番号付けの選び方（計算可能に読み戻せること）$\#$ に計算可能でない全単射 $\pi\colon\mathbb N\to\mathbb N$ を合成した $\pi\circ\#$論理式の番号の集合が原始再帰的であること
反例の確かめ

1 行目：等式は $f(y)=f(y)$ と同じなので、すべての関数 $f$ が満たす。とくに計算可能でない集合 $K$ の特性関数 $\chi_K$ も満たし、$\chi_K$ は原始再帰関数でない（原始再帰関数は計算可能である。原始再帰関数 の記事の節「補足：計算可能性との関係」）。計算可能でない集合があることは 停止問題 の記事の定理「停止問題の決定不能性」による。
2 行目：$f(y)=h(y,\bar f(y))=\chi_K(y)$ なので $f=\chi_K$ であり、1 行目と同じ理由で原始再帰的でない。
3 行目：$K$ を計算可能でない集合とし、$B:=\{2k\mid k\in K\}\cup\{2k+1\mid k\notin K\}$ とおく。どの $k$ についても $2k,2k+1$ のちょうど一方が $B$ に属するので、$B$ も補集合も無限集合である。$k\in K\iff 2k\in B$ なので、$B$ が計算可能なら $K$ も計算可能になり矛盾する。論理式の Gödel 数の集合 $\#\mathrm{Fm}$ も補集合も無限集合なので（$v_0=v_0,\ v_1=v_1,\dots$ は相異なる論理式で、項の Gödel 数は論理式の Gödel 数でない）、$\#\mathrm{Fm}$ を $B$ へ、補集合を補集合へ、それぞれ小さい順に対応させる全単射 $\pi$ がある。$\pi\circ\#$ は項と論理式に単射に番号を付けるが、論理式の番号の集合 $\pi(\#\mathrm{Fm})=B$ は計算可能でなく、とくに原始再帰的でない。単射であることだけでは、Gödel 数化として役に立たない。

補足

  • 記号列による番号付け：OLT26 第 34 章は、記号に番号を付け、記号列を番号の列として符号化する。そこでも、項・論理式・文であること（Proposition 34.5・34.8・34.10、pp. 535–537）、数項（Proposition 34.6、p. 536）、代入（Proposition 34.11、p. 538）が原始再帰的であることが示されている。木の符号と記号列の符号のどちらを使っても、上の定理はそのまま成り立つ。
  • 機械とプログラムの番号付け：万能Turing機械 の記事は、同じ列の符号で Turing 機械に番号を付け、計算の 1 ステップを原始再帰関数で書く。これも Gödel 数化の一種で、プログラムをデータとして扱う万能機械の構成の土台になる。
  • 算術の中での表現：原始再帰的な関係は、算術の言語の論理式で弱い算術 $\mathsf Q$ の中で表現できる（Gödelの不完全性定理 の記事の注意「この記事では証明しない事実」の 1）。この記事の定理と合わせると、$\operatorname{Fm}$・$d$・$\operatorname{Prf}_T$ などが算術の論理式で表現され、構文についての主張が算術の文になる。

関連項目

参考文献

Mathpediaは寄付と、参考文献の書籍リンク（Amazonアソシエイト）の紹介料で運営されています。 支援について ／ 寄付する

Mathpediaを支援する
Gödel数化