| 1.数学的理論の形式化 1 |
| 1.0 形式化される数学的理論の概要 1 |
| 1.1 記号 2 |
| 1.2 対象式 4 |
| 1.3 論理式 4 |
| 1.4 自由変数への対象式の代入 7 |
| 1.5 公理 9 |
| 1.6 推論の規則 11 |
| 2.命題論理 13 |
| 2.1 →について 13 |
| 2.2 仮定をもつ推論(仮定が1つの論理式である場合) 15 |
| 2.3 仮定をもつ推論(一般の場合) 16 |
| 2.4 ￢について 20 |
| 2.5 論理式の同値 23 |
| 2.6 ∧について 28 |
| 2.7 Λについて 31 |
| 2.8 ←→について 34 |
| 3.述語論理 38 |
| 3.1 ∀について 38 |
| 3.2 ∃について 41 |
| 3.3 限定作用素の順序の交換 44 |
| 3.4 束縛変数の書きかえ 45 |
| 3.5 仮定をもつ推論 50 |
| 4.等号をもつ述語論理 54 |
| 4.1 等号の基本性質 54 |
| 4.2 ∃!について 57 |
| 4.3 ι-記号 59 |
| 4.4 ι-記号の使用法についての諸定理61 |
| 4.5 対象式の概念の拡張 68 |
| 5.型の理論 72 |
| 5.1 型の理論の公理 72 |
| 5.2 簡単な集合論的記法 73 |
| 6.自然数論 79 |
| 6.1 自然数の公理 79 |
| 6.2 関数の帰納的定義 80 |
| 6.3 加法の性質 86 |
| 6.4 乗法の性質 88 |
| 6.5 大小関係 91 |
| 6.6 ε-記号 96 |
| 7.自然数の関係および関数について形式的な表現の可能性 98 |
| 7.0 用語・記号について規約 99 |
| 7.1 関係の形式的な表現可能性 101 |
| 7.2 関数の形式的な表現可能性 106 |
| 7.3 表現可能な関係・関数の例 114 |
| 8.ゲーデルの不完全性定理 117 |
| 8.1 ゲーデル数 118 |
| 8.2 証明の形式化 121 |
| 8.3 Bewk(x)の性質I 125 |
| 8.4 ω-無矛貭性 Bewk(x)の性質II 127 |
| 8.5 ゲーデルの対角化定理 130 |
| 8.6 ゲーデルの不完全性定理 133 |
| 8.7 '嘘つき'のパラドックス タルスキー定理 137 |
| 8.8 ロッサーの不完全性定理 139 |
| 9.補助定理の証明 143 |
| 9.1 補助定理IIIの証明 143 |
| 9.2 補助定理IIの証明 144 |
| 9.3 補助定理Iの証明 149 |
| 10.ゲーデルの第2不完全性定理 153 |
| 10.1 関係および関数の強い意味での表現可能性 153 |
| 10.2 ゲーデルの第2不完全性定理 155 |
| 10.3 公式10.1の証明の方針 157 |
| 10.4 公式10.7の証明の概要 159 |
| 10.5 クライゼルの注意 162 |
| 11.帰納的関数 164 |
| 11.1 一般帰納的関数 164 |
| 11.2 帰納的関数の基本的な性質 168 |
| 11.3 表現可能性との一致 173 |
| 11.4 チャーチの提唱 177 |
| 11.5 証明可能性についての決定問題 181 |
| 12.帰納的関数の性質 184 |
| 12.1 算術的な関係 184 |
| 12.2 算術的な論理式 188 |
| 12.3 帰納的関係・帰納的関数の標準形 190 |
| 12.4 Bv,Tv,Uが原始帰納的であることの証明 193 |
| 12.5 原始帰納的関数の強い意味での表現可能性 195 |
| 記号表 198 |
| 索引 199 |
図書
図書
