数学 › 数理論理学と型理論 › 計算可能性

クリーネの標準形定理

定理 5.3（「計算可能性」§5）・ ✓公理まで証明済み

各 $n\ge1$ に対して、原始再帰的な述語 $T_n(e,\vec{x},t)$ と原始再帰的な関数 $U(c)$ が存在して、すべての $e,\vec{x}$ について

\varphi^{(n)}_e(\vec{x})\ \simeq\ U\bigl(\mathrm{Conf}(e,\vec{x},\ \mu t\,[T_n(e,\vec{x},t)])\bigr)

が成り立つ。ここで $\mathrm{Conf}(e,\vec{x},t)$ は、 $M_e$ を標準入力 $\vec{x}$ から $t$ ステップ動かした後の状況の符号である。

本文で読む（証明と前後の説明）→

閉包の状態

✓ 公理まで証明済み

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

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

前提をたどる証明が使う定理・定義（直接 1 件）

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

1 ステップの算術化✓補題 5.2・計算可能性
- 機械の番号定義 5.1・計算可能性
- 原始再帰関数の道具箱✓命題 3.2・計算可能性
  - ユークリッドの定理✓定理 3.2・素数の魅力と素数定理
    最小の約数は素数✓補題 3.1・素数の魅力と素数定理

これを使っている定理証明で参照している 3 件

チューリング計算可能なら部分再帰的✓定理 5.4・計算可能性
停止問題の補集合は半決定可能でない✓系 7.3・計算可能性
再帰関数の全関数による生成✓補題 6.5・型なしラムダ計算

関連するノック 2 問