【数学】RCA0上で再帰的定義が可能なことの証明

はにゃ

逆数学のセミナーで、 RCA$_0$に於いて再帰定義ができるのかわからず困ってしまったので覚書を作りました。

RCA$_0$ とは、離散的順序半環の公理であるところの PA$^-$ に$\Delta_0$ comprehension axiom と $\Sigma_10$ 式までの帰納法を認めた体系です。

本質部分は殆ど [田中19] によるのですが、 細かい注釈と式の気持ちをかなり補ったのでギリギリ公開する価値があるかなと思い、 公開いたします。



ねるにゃ!。



[追記 2024/12/24 04:01] 命題0.3 は当然メタの主張です。
[追記 2024/12/24 15:07] 追記しました。