クリーネの定理（λ 定義可能性と再帰性）

定理 6.4（「型なしラムダ計算」§6）・ ✓公理まで証明済み

全関数 $\varphi:\mathbb{N}^k\to\mathbb{N}$ について、 $\varphi$ が再帰関数（定義 4.1［計算可能性］の意味で、全関数である部分再帰関数）であることと、λ 定義可能であることは同値である。

閉包の状態

✓ 公理まで証明済み

証明が使う定理を前提としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 15 件、定義なども含めて 19 件）。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。

▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。

再帰関数の全関数による生成✓補題 6.5・型なしラムダ計算
- 部分再帰関数はチューリング計算可能✓定理 6.2・計算可能性
- クリーネの標準形定理✓定理 5.3・計算可能性
  - 1 ステップの算術化✓補題 5.2・計算可能性
    機械の番号定義 5.1・計算可能性
    原始再帰関数の道具箱✓命題 3.2・計算可能性（上で展開済み）
チャーチ数・真偽値・組の基本項✓補題 6.2・型なしラムダ計算
ゲーデル数定義 4.1・ゲーデルの不完全性定理
β 簡約の算術化✓補題 6.6・型なしラムダ計算
- 原始再帰関数の道具箱✓命題 3.2・計算可能性（上で展開済み）
- 置換定義 2.2・型なしラムダ計算
- β 簡約定義 3.1・型なしラムダ計算
原始再帰関数の道具箱✓命題 3.2・計算可能性
- ユークリッドの定理✓定理 3.2・素数の魅力と素数定理
  - 最小の約数は素数✓補題 3.1・素数の魅力と素数定理
チャーチ＝ロッサーの帰結✓系 4.6・型なしラムダ計算
- チャーチ＝ロッサーの定理✓定理 4.1・型なしラムダ計算
  - 三角補題✓補題 4.5・型なしラムダ計算
    並行簡約と置換✓補題 4.4・型なしラムダ計算この先をたどる →
  - 並行簡約の基本性質✓補題 4.3・型なしラムダ計算

証明で明示的に参照している定理は、まだありません。