タルスキの定義不可能性定理
解釈された言語は、その言語がその言語に特有の意味論的概念を定義する述語と関数記号を含むときちょうど strongly-semantically-self-representational となる。したがって、要求されている関数は式 A をその 真理値 ||A|| に対応させる"意味論的評価関数"と項 t をその対象に対応させる"意味論的指示関数"を含む。タルスキの定理は次のように一般化される:十分に強い言語は strongly-semantically-self-representational にはなりえない。
定義不可能性定理はある理論における真理がより強い理論において定義されることを妨げるわけではない。例えば、一階述語のペアノ算術の式(のコード)で N において真になるものの集合は二階算術の式で定義可能である。同様に、二階算術 (あるいはそれより上の高階算術) の標準モデルにおいて真になる式の集合は一階述語である ZFC の式で定義できる。
タルスキは完全に構文的な手法を用いて、上記よりも強い定理を証明している。その定理は否定を持ち対角線補題(英語版)が成立する程度に自己言及できる十分な強さを持ついかなる形式言語にも適用できる。一階算術はそういった前提条件を満たすが、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 が反例となる。これは矛盾である。