>>215 補足
>ゲーデルの不完全性定理よりも定義不可能性定理のほうが根源的でしかも易しい
>（わざわざ証明可能性述語を具体的に構成する必要がないので）

ホイヨ
下記の＜AI による概要＞
タルスキの定義不可能性定理
「この定理は、ゲーデルの不完全性定理 と並び、形式体系が持つ能力の限界を示す重要な成果である」
とありますぜ、ダンナｗ　（＾＾
つまり ”ゲーデルの不完全性定理よりも定義不可能性定理のほうが根源的でしかも易しい”
とは、ちょっと違うのでは？ｗ

(google検索)
タルスキの定義不可能性定理
＜AI による概要＞
タルスキの定義不可能性定理（Tarski's undefinability theorem）は、十分な能力を持つ形式体系（算術など）において、「真理」という概念はその体系自身の中では定義できないことを示す数学基礎論の定理。1933年にアルフレト・タルスキにより証明され、自身の体系で自身の真偽を判定できない限界を明らかにした。
定理の要点
・算術的真理の定義不可: 自然数論のような一定の強さを持つ形式体系では、その体系内での「真なる文」の集合を、その体系自身の論理式として定義できない。
・定義しようとすると矛盾する: 真理を定義しようとすると、論理的な矛盾（例えば、自己言及パラドックスのような状態）が生じる。
・言語の階層: ある言語（体系）の真理は、より高階の言語（メタ言語）でのみ定義可能となる。
この定理は、ゲーデルの不完全性定理 と並び、形式体系が持つ能力の限界を示す重要な成果である。