自己言及の構成 (対角化補題)

対角化補題は、十分に表現力のある形式体系で、ある性質を自分自身のコードに適用する文を構成できることを示す。自己言及を厳密な構文操作へ落とすため、不完全性や決定不能性の証明に使われる。

式・証明・プログラムを自然数などへ符号化し、置換を表す関数を体系内で表現する。自己適用を含む文を作った後、意味論上の解釈と体系内の導出を区別して追う。

自己言及は日常語の循環論法ではない。符号化可能性と表現力という前提が必要で、すべての再帰的定義やメタデータ参照が直ちに矛盾を生むわけではない。