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

タルスキの定義不可能性定理は、1933年にアルフレッド・タルスキによって提唱され証明されたもので、数理論理学、数学の基礎、形式意味論における重要な極限結果である。非公式には、この定理は「算術的真理は算術では定義できない」と述べている。^{[ 1 ]}

この定理は、十分に強力な形式体系であればどのようなものにもより一般的に適用され^、その体系の標準モデルにおける真理は体系内で定義できないことを示している。^{[ 2 ]： 491、493}

1931年、クルト・ゲーデルは不完全性定理を発表した。彼は、形式論理の構文を一階算術で表現する方法を示すことで、その定理の一部を証明した。算術の形式言語の各式には、それぞれ異なる番号が割り当てられる。この手順は、ゲーデル番号付け、符号化、より一般的には算術化など、さまざまな名称で知られている。特に、さまざまな式の集合が数値の集合として符号化される。これらの集合は、さまざまな構文特性（式であること、文であることなど）に関して計算可能である。さらに、任意の計算可能な数値の集合は、何らかの算術式によって定義できる。例えば、算術の言語には、算術文の符号の集合、および証明可能な算術文（計算可能な列挙可能な集合）の符号の集合を定義する式が存在する。

定義不可能性定理は、真理などの意味概念に対してこのような符号化は不可能であることを示している。それは、十分に豊かな解釈言語は、自身の意味を表現できないことを示している。その帰結として、ある対象言語の意味を表現できるメタ言語（例えば、ツェルメロ・フレンケル集合論では、ペアノ算術の言語における式が標準的な自然数算術モデルにおいて真であるかどうかの述語を定義できる^{[ 3 ]}）は、対象言語の表現力を超える表現力を持たなければならない。メタ言語には、対象言語には存在しない原始概念、公理、推論規則が含まれるため、対象言語では証明できない定理がメタ言語では証明可能となる。

定義不可能性の定理は、一般的にアルフレッド・タルスキに帰せられている。ゲーデルもまた、1930年に定義不可能性の定理を発見しており、これは1931年に発表された不完全性定理を証明する過程で、タルスキの著作が1933年に発表されるずっと前のことである（ムラフスキ 1998）。ゲーデルは定義不可能性の独立した発見に関する著作を一切発表しなかったが、1931年にジョン・フォン・ノイマンに宛てた手紙の中でそのことを述べている。タルスキは、1933年の著書『演繹科学の言語における真理の概念』のほぼすべての結果を1929年から1931年の間に得ており、ポーランドの聴衆に向けてそれらについて語っていた。しかし、論文の中で彼が強調したように、定義不可能性の定理は彼がそれ以前に得ていなかった唯一の結果であった。 1933年のモノグラフの不確定性定理（ Twierdzenie I ）の脚注によると、定理と証明の概略は、原稿が1931年に印刷所に送られた後にモノグラフに追加された。タルスキはそこで、1931年3月21日にワルシャワ科学アカデミーでモノグラフの内容を発表した際、この箇所では、自身の調査とゲーデルの不完全性定理に関する短い報告「決定の確定性と一貫性に関するいくつかのメタ数学的結果」、オーストリア科学アカデミー、ウィーン、1930年に基づいて、いくつかの推測のみを述べたと報告している。

まず、タルスキの定理の簡略版を述べ、次に、タルスキが1933年に証明した定理を次の節で述べ、証明する。

させて${\displaystyle L}$これは一階算術の言語である。これは、自然数の加算と乗算を含む自然数の理論であり、一階ペアノ公理によって公理化されている。これは「一階」理論である。量化子は自然数に及ぶが、自然数の集合や関数には及ばない。この理論は、べき乗、階乗、フィボナッチ数列などの再帰的に定義された整数関数を記述するのに十分な強度を持つ。

させて${\displaystyle \mathbb {N} }$標準構造となる${\displaystyle L}$つまり${\displaystyle \mathbb {N} }$は、通常の自然数とその加算と乗算の集合から成ります。${\displaystyle L}$解釈できる${\displaystyle \mathbb {N} }$そして真か偽かのどちらかになる。したがって${\displaystyle (L,\mathbb {N} )}$これは「解釈可能な一階述語論理による算術言語」である。

各式${\displaystyle \varphi }$で${\displaystyle L}$ゲーデル数を持つ${\displaystyle g(\varphi )}$これは「エンコード」された自然数です${\displaystyle \varphi }$そういう意味で、言語は${\displaystyle L}$数式について話すことができます${\displaystyle L}$数字だけの話ではない。${\displaystyle T}$の集合を表す${\displaystyle L}$-文は正しい${\displaystyle \mathbb {N} }$、 そして${\displaystyle T^{*}}$ the set of Gödel numbers of the sentences in ${\displaystyle T}$. The following theorem answers the question: Can ${\displaystyle T^{*}}$ be defined by a formula of first-order arithmetic?

Tarski's undefinability theorem (simplified form): There is no ${\displaystyle L}$-formula ${\displaystyle \mathrm {True} (n)}$ that defines ${\displaystyle T^{*}}$. That is, there is no ${\displaystyle L}$-formula ${\displaystyle \mathrm {True} (n)}$ such that for every ${\displaystyle L}$-sentence ${\displaystyle A}$, the formula ${\displaystyle \mathrm {True} (g(A))\iff A}$ holds in ${\displaystyle \mathbb {N} }$.

Informally, the theorem says that the concept of truth of first-order arithmetic statements cannot be defined by a formula in first-order arithmetic. This implies a major limitation on the scope of "self-representation". By working in a stronger system (e.g., by adding a sort of subsets of ${\displaystyle \mathbb {N} }$ as in second-order arithmetic) it is possible to define a formula ${\displaystyle \mathrm {True} (n)}$ that holds on exactly the set ${\displaystyle T^{*}}$, but that does not define truth for the stronger system: this formula ${\displaystyle \mathrm {True} (n)}$ only defines a truth predicate for formulas in the original language ${\displaystyle L}$ (e.g., because ${\displaystyle T^{*}}$ does not contain codes for sentences quantifying over subsets of ${\displaystyle \mathbb {N} }$). To define truth in this stronger system would require ascending to an even stronger system and so on.

To prove the theorem, we proceed by contradiction and assume that an ${\displaystyle L}$-formula ${\displaystyle \mathrm {True} (n)}$ exists that is true for the natural number ${\displaystyle n}$ in ${\displaystyle \mathbb {N} }$ if and only if ${\displaystyle n}$ is the Gödel number of a sentence in ${\displaystyle L}$ that is true in ${\displaystyle \mathbb {N} }$. We could then use ${\displaystyle \mathrm {True} (n)}$ to define a new ${\displaystyle L}$-formula ${\displaystyle S(m)}$ that is true for the natural number ${\displaystyle m}$ if and only if ${\displaystyle m}$ is the Gödel number of a formula ${\displaystyle \varphi (x)}$ (with a free variable ${\displaystyle x}$) such that ${\displaystyle \varphi (m)}$ is false when interpreted in ${\displaystyle \mathbb {N} }$ (i.e. the formula ${\displaystyle \varphi (x)}$, when applied to its own Gödel number, yields a false statement). If we now consider the Gödel number ${\displaystyle g}$ of the formula ${\displaystyle S(m)}$, and ask whether the sentence ${\displaystyle S(g)}$ is true in ${\displaystyle \mathbb {N} }$, we obtain a contradiction. (This is known as a diagonal argument.)

The theorem is a corollary of Post's theorem about the arithmetical hierarchy, proved some years after Tarski (1933). A semantic proof of Tarski's theorem from Post's theorem is obtained by contradiction as follows. Assuming ${\displaystyle T^{*}}$ is arithmetically definable, there is a natural number ${\displaystyle n}$ such that ${\displaystyle T^{*}}$ is definable by a formula at level ${\displaystyle \Sigma _{n}^{0}}$ of the arithmetical hierarchy. However, ${\displaystyle T^{*}}$ is ${\displaystyle \Sigma _{k}^{0}}$-hard for all ${\displaystyle k}$. Thus the arithmetical hierarchy collapses at level ${\displaystyle n}$, contradicting Post's theorem.

Tarski proved a stronger theorem than the one stated above, using an entirely syntactical method. The resulting theorem applies to any formal language with negation, and with sufficient capability for self-reference that the diagonal lemma holds. First-order arithmetic satisfies these preconditions, but the theorem applies to much more general formal systems, such as ZFC.

Tarski's undefinability theorem (general form): Let ${\displaystyle (L,{\mathcal {N}})}$否定を含み、ゲーデル数を持つ任意の解釈可能な形式言語とする。${\displaystyle g(\varphi )}$対角補題を満たす、すなわち、すべての${\displaystyle L}$-式${\displaystyle B(x)}$（自由変数1つ付き）${\displaystyle x}$) 文があります${\displaystyle A}$そのため${\displaystyle A\iff B(g(A))}$保持する${\displaystyle {\mathcal {N}}}$そうすれば${\displaystyle L}$-式${\displaystyle \mathrm {True} (n)}$次の性質を持つ：${\displaystyle L}$-文${\displaystyle A,}$式${\displaystyle \mathrm {True} (g(A))\iff A}$は真実です${\displaystyle {\mathcal {N}}}$。

この形式のタルスキの不確定性定理の証明は、再び背理法による。${\displaystyle L}$-式${\displaystyle \mathrm {True} (n)}$上記のように存在していた場合、つまり、${\displaystyle A}$は${\displaystyle L}$-文、それから${\displaystyle \mathrm {True} (g(A))}$保持する${\displaystyle {\mathcal {N}}}$かつその場合に限り${\displaystyle A}$保持する${\displaystyle {\mathcal {N}}}$したがって、すべての${\displaystyle A}$式${\displaystyle \mathrm {True} (g(A))\iff A}$保持する${\displaystyle {\mathcal {N}}}$しかし、対角線補題では、${\displaystyle B(x)}$インスタンス化${\displaystyle \lnot \mathrm {True} (x)}$は、「嘘つき」の公式を与えることで、この等価性に対する反例を与える。${\displaystyle S}$そのため${\displaystyle S\iff \lnot \mathrm {True} (g(S))}$保持する${\displaystyle {\mathcal {N}}}$これは矛盾である。証明終了。

上記の証明の形式的な仕組みは、対角補題に必要な対角化を除いて、完全に初等的です。対角補題の証明も同様に驚くほど単純で、例えば、いかなる形でも再帰関数は使用されていません。証明では、すべての${\displaystyle L}$-式はゲーデル数を持つが、符号化方法の具体的な内容は必要ない。したがって、タルスキーの定理は、一階算術のメタ数学的性質に関するゲーデルのより有名な定理よりも、動機付けや証明がはるかに容易である。

スムリアン（1991、2001）は、タルスキの定義不可能性定理はゲーデルの不完全性定理が受けた注目に値すると力強く主張している。後者の定理が数学全体、そしてより議論の余地のある哲学的問題（例えば、ルーカス1961）について多くを語っていることは、それほど明白ではない。一方、タルスキの定理は直接数学に関するものではなく、真に興味を抱かせるほど十分に表現力のある形式言語の固有の限界に関するものである。そのような言語は、対角線補題を適用するために十分な自己参照能力を必然的に備えている。タルスキの定理のより広範な哲学的意義は、より顕著に明らかである。

解釈型言語は、その言語に固有のすべての意味概念を定義する述語と関数記号が含まれている場合に、意味的に強く自己表現的であると言えます。したがって、必要な関数には、式をマッピングする「意味評価関数」が含まれます。${\displaystyle A}$その真実性に対して${\displaystyle ||A||}$、そして用語をマッピングする「意味的指示関数」${\displaystyle t}$タルスキの定理は次のように一般化される。十分に強力な言語は、意味的に強く自己表現的ではない。

The undefinability theorem does not prevent truth in one theory from being defined in a stronger theory. For example, the set of (codes for) formulas of first-order Peano arithmetic that are true in ${\displaystyle {\mathcal {N}}}$ is definable by a formula in second-order arithmetic. Similarly, the set of true formulas of the standard model of second-order arithmetic (or ${\displaystyle n}$th-order arithmetic for any ${\displaystyle n}$) can be defined by a formula in first-order ZFC.

• Atopy (philosophy) – Impracticality of being assimilated to a topic
• Chaitin's incompleteness theorem – Measure of algorithmic complexityPages displaying short descriptions of redirect targets
• Cognitive closure (philosophy) – Inherent limitations of the human mind
• Gödel's completeness theorem – Fundamental theorem in mathematical logic
• Gödel's incompleteness theorems – Limitative results in mathematical logic
• Ignoramus et ignorabimus – Maxim about limits of scientific knowledge
• Ineffability – Inability of an idea or feeling to be expressed with words
• Unknowability – Philosophical idea of things impossible to know

• Bell, JL; Machover, M. (1977).数理論理学入門. North-Holland.
• Boolos, G. ; Burgess, J. ; Jeffrey, R. (2002).計算可能性と論理（第4 版）. Cambridge University Press.
• ルーカス、JR（1961）。「心、機械、そしてゲーデル」。Philosophy。36 （ 137）：112–27。doi：10.1017 /S0031819100057983。hdl：10077/5466。S2CID 55408480。 2007年8月19日にオリジナルからアーカイブ済み。 
• ムラウスキー、R. (1998). 「真理の定義不可能性。優先権の問題：タルスキ対ゲーデル」 .論理学の歴史と哲学. 19 (3​​): 153–160 . doi : 10.1080/01445349808837306 . 2011年6月8日にオリジナルからアーカイブ済み。
• スムリアン、レイモンド・M. (1992).ゲーデルの不完全性定理. オックスフォード：オックスフォード大学出版局、米国。ISBN 0-19-504672-2。
• スムリアン、R. (2001). 「ゲーデルの不完全性定理」. ゴブル、L. (編) 『ブラックウェル哲学論理学ガイド』 . ブラックウェル. pp. 72–89 . ISBN  978-0-631-20693-4。