タルスキの定義不可能性定理

タルスキの定義不可能性定理 (Tarski's undefinablity theorem)とは1933年にアルフレト・タルスキによって提唱・証明された数理論理学、数学基礎論、形式意味論における重要な限界を示した結果である。大まかに言えば、この定理は算術的な真理を算術内で定義することはできないことを主張する。

この定理はより一般に、十分に強い形式体系にも適用でき、その体系の標準モデルでの真偽をその体系内で定義できないことを示す。

歴史

1931年、クルト・ゲーデルはゲーデルの不完全性定理を発表した。この定理は形式論理の構文を一階算術で表現する方法を示すことで証明された。算術の形式言語の各表現には個別の番号を割り振ることができ、この手続きはゲーデル数化、コード化、より一般に算術化などと呼ばれて知られている。特に、様々な式の集合は数の集合としてコード化される。様々な構文的性質（式であること、文であること、など）について、これらの集合は帰納的集合である。さらに、数の計算可能な集合は何らかの算術的な式によって定義することができる。例えば、算術の言語には算術式や証明可能な算術文のコードの集合を定義する式がある。

定義不可能性定理は、真理のような意味論的概念をこのようにコード化することができないことを示す。これは、十分に豊かに解釈される言語で、自身の意味論を表現できるものはないことを示している。このことから、対象言語の意味論を表現できるようなメタ言語は、その対象言語の意味論を超える表現能力を持たなければならないことになる。メタ言語は、対象言語にはない原始概念、公理、規則を含んでおり、対象言語では証明できない定理であってメタ言語では証明可能であるものがある。

この定義不可能性定理はこれまでアルフレト・タルスキによるものとされてきたが、ゲーデルもまた、1931年に発表した不完全性定理の証明の中で、1930年に定義不可能性定理を発見している。これは1933年に発表したタルスキよりもかなり前である。ゲーデルは独立に定義不可能性を発見したことに関して発表することはなかったが、1931年にジョン・フォン・ノイマンに宛てた手紙の中では触れている。タルスキは1933年のモノグラフ "The Concept of Truth in the Languages of the Deductive Sciences" にあるほとんどの結果は1929年から1931年にかけて得ており、ポーランドの聴衆にこれらのことを話している。しかしながら、論文の中で彼が強調したように、定義不可能性定理だけはそれ以前に得られていない結果であった。その1933年のモノグラフの定義不可能性定理 (Twierdzenie I) の脚注によれば、この定理と証明のスケッチは、1931年に原稿が印刷所に送られた後モノグラフに追加されたものである。タルスキは、1931年3月21日にワルシャワ科学アカデミーにおいて自身のモノグラフの内容を講演したときに、ゲーデルの不完全性定理に関する短い報告と自身の独自研究に一部基づくいくつかの予想をその場で話しただけであると報告している。

定理の主張

初めにタルスキの定理の簡略版を述べてから、次節でタルスキが1933年に証明した定理を述べ、証明することにする。

L を一階算術の語彙とする。ここでいう一階算術は加法と乗法を含みペアノの公理で公理化された自然数についての理論である。"一階"の理論とはすなわち、自然数全体にわたる量化はあるが、自然数全体の部分集合や自然数上の関数は量化の対象にしないものである。この理論は指数関数や階乗、フィボナッチ数列など再帰的な整数関数を記述するのに十分な強さをもった理論である。

N を L の標準構造とする。すなわち N は普通の自然数全体とその上の加法と乗法からなるものとする。L の各式は N において解釈され、真か偽かが決定される。そこで (L, N) は"解釈された一階算術の語彙"である。

L の各式 φ はゲーデル数 g(φ) を持つ。これは φ を"コード化"する自然数である。このようにして、語彙 L は数だけでなく L の式について語ることができる。 T を N で真になるような L-文の集合とする。そして、T* を T に属する文のゲーデル数全体とする。次の定理は、「 T* は一階算術の式で定義できるだろうか」という問いに答えるものである。

タルスキの定義不可能性定理 ― T* を定義する L-式 True(n) は存在しない。 すなわち、L-式 True(n) で、全ての L-文 A に対して True(g(A)) ↔ A が N で成り立つようなものは存在しない。

この定理は、大まかに言えば、一階算術の文の真理の概念を一階算術の式で定義できないことを主張する。これは"自己表現"の範囲における重要な制限を意味する。True(n) を定義すること自体は可能であるが、それは L を超える表現力を持つメタ言語を引き合いに出すことによってのみ可能である。例えば、一階算術の真理述語は二階算術の中で定義することが可能である。しかしながら、この式は元々の語彙 L の真理述語しか定義できない。メタ言語の真理述語を定義するには、さらに高位のメタ言語を必要とする、といった具合になる。

この定理を証明するために、背理法で進める。

証明 — 示すべきことに反し、L-式 True(n) が存在して以下を満たすと仮定する：N で真である L-文のゲーデル数が n であるときかつそのときに限り True(n) が真である。このとき、True(n) を用いて新しい L-式 S(m) を次のように定義することができる：m が式 φ(x) （x は自由変数）のゲーデル数であって φ(m) が N において偽であるときかつそのときに限り S(m) が真である（すなわち、自身のゲーデル数を代入したときに偽になる式 φ(x) を考える）。 ここで、S(m) のゲーデル数 g を考え、S(g) は N で真かどうかを問うと矛盾を生ずる（これはいわゆる対角線論法である）。

この定理は算術的階層におけるポストの定理の系でもある。ポストの定理からタルスキの定理の意味論的証明を得るには以下のような背理法を用いる。T* が算術的定義可能であると仮定すると、ある自然数 n について、T* は算術的階層のレベル $\Sigma _{n}^{0}$ の式によって定義することができる。しかしながら、T* は全ての k に対して $\Sigma _{k}^{0}$-困難である。ゆえに算術的階層がレベル n で破綻していてこれがポストの定理に反する。

一般的な形

タルスキは完全に構文的な手法を用いて、上記よりも強い定理を証明している。その定理は否定を持ち対角線補題が成立する程度に自己言及できる十分な強さを持ついかなる形式言語にも適用できる。一階算術はそういった前提条件を満たすが、ZFC のようなもっと一般的な形式体系にも適用できる。

タルスキの定義不可能性定理 (一般形) ―  (L,N) を否定を持つ形式言語の解釈されたものとして、そこでのゲーデル数化 g(φ) が対角線補題を満たすものとする。すなわち、全ての L-式 B(x) （一つの自由変数 x をもつもの）に対して、文 A で A ↔ B(g(A)) が N で成立するものがある。このとき、L-式 True(n) で次の性質を満たすようなものは存在しない：全ての L-文 A に対して True(g(A)) ↔ A が N において成り立つ。

この形のタルスキの定義不可能性定理でも同様に背理法で証明できる。

証明 — L-式 True(n) が上で述べた性質を満たすものとして存在したとする。すなわち、A が算術の文であるときに True(g(A)) が N で真であるときかつそのときに限り A が N において真である。つまり、全ての A に対して式 True(g(A)) ↔ A が N において成立する。しかし、その同値性に対しては対角線補題によって S ↔ ¬True(g(S)) が N において成り立つ"嘘つき"式 S が反例となる。これは矛盾である。

議論

上で与えられた証明の形式的な仕組みは、対角線補題で用いられる対角化を除いて全く初歩的なものである。対角線補題自体の証明も驚くほど単純であり、例えば再帰関数などは不要である。この証明では全ての L-式がゲーデル数を持つと仮定するが、具体的なコーディング内容は要求されない。したがってタルスキの定理は、一階算術のメタ数学的性質に関するゲーデルの不完全性定理よりも動機づけと証明はずっと簡単である。

レイモンド・スマリヤンは、タルスキの定義不可能性定理はゲーデルの不完全性定理が集めた注目に値すると強く主張している。ゲーデルの定理が、全ての数学やもっと議論を呼ぶ哲学的問題の範囲について多くを語れるかどうかはあまり明らかでない。一方でタルスキの定理は直接的に数学に関するものでなく、実際の興味を持つに足る十分な表現能力のある全ての形式言語の先天的な限界に関するものである。そのような言語は対角線補題を適用できる程度の自己言及が必然的に可能である。タルスキの定理の広範な哲学的意義はより明らかである。

解釈された言語は、その言語がその言語に特有の意味論的概念を定義する述語と関数記号を含むときちょうど strongly-semantically-self-representational となる。したがって、要求されている関数は式 A をその 真理値 ||A|| に対応させる"意味論的評価関数"と項 t をその対象に対応させる"意味論的指示関数"を含む。タルスキの定理は次のように一般化される：十分に強い言語は strongly-semantically-self-representational にはなりえない。

定義不可能性定理はある理論における真理がより強い理論において定義されることを妨げるわけではない。例えば、一階述語のペアノ算術の式（のコード）で N において真になるものの集合は二階算術の式で定義可能である。同様に、二階算術 (あるいはそれより上の高階算術) の標準モデルにおいて真になる式の集合は一階述語である ZFC の式で定義できる。

関連項目

• ゲーデルの不完全性定理

参考文献

• J. L. Bell, and M. Machover, 1977. A Course in Mathematical Logic. North-Holland.
• G. Boolos, J. Burgess, and R. Jeffrey, 2002. Computability and Logic, 4th ed. Cambridge University Press.
• J. R. Lucas, 1961. "Mind, Machines, and Gödel". Philosophy 36: 112–27.
• R. Murawski, 1998. Undefinability of truth. The problem of the priority: Tarski vs. Gödel. History and Philosophy of Logic 19, 153–160
• R. Smullyan, 1991. Godel's Incompleteness Theorems. Oxford Univ. Press.
• R. Smullyan, 2001. "Gödel’s Incompleteness Theorems". In L. Goble, ed., The Blackwell Guide to Philosophical Logic, Blackwell, 72–89.
• A. Tarski, 1933. Pojęcie Prawdy w Językach Nauk Dedukcyjnych. Nakładem Towarzystwa Naukowego Warszawskiego.
• A. Tarski (1936). “Der Wahrheitsbegriff in den formalisierten Sprachen”. Studia Philosophica 1: 261–405. オリジナルの9 January 2014時点におけるアーカイブ。. https://web.archive.org/web/20140109135345/http://www.ifispan.waw.pl/studialogica/s-p-f/volumina_i-iv/I-07-Tarski-small.pdf 26 June 2013閲覧。. 
  • A. Tarski, tr. J. H. Woodger, 1983. "The Concept of Truth in Formalized Languages". English translation of Tarski's 1936 article. In A. Tarski, ed. J. Corcoran, 1983, Logic, Semantics, Metamathematics, Hackett.