logicBye - 41semicolon/41semicolon.github.io GitHub Wiki

ルイスキャロルのパラドックス: 体系を特徴づけるためには計算可能性が必要。「これが公理であるか」とか「これは正しい推論規則の適用なのか」という判断が機械的でなければ無限後退に陥るため（→ルイスキャロルのパラドックス）。そして「機械的な判断」という概念を計算可能性（決定手続きや再帰関数やチャーチ＝チューリング＝のテーゼ等々）で特徴づける。こうするとQなどを定理生成器とみなす描像を正当化できるし、PAのような公理図式を持つ理論をきちんと取り扱える

可証性述語の定義可能性: 可証性述語はΠ1という比較的単純な算術階層の論理式で定義可能。この事実は真理述語の定義不可能性（タルスキの定理）と対照的。一方Σ1文に限定した真理述語であれば定義可能であり、しかもそれが（少なくとも外延的には）可証性述語と同一視できるという事実をもって、「第一不完全性定理は真理述語の定義不可能性の表れのひとつとみなせる」という解釈が可能(→照井)