■

前回、最小算術 Q の断片（大小関係に関する公理を除去したもの）の公理系を紹介し、これである程度数学を展開するための道具は揃いました。それでは、授業第十一回目の今回、この枠組みの中で、簡単な算数の証明がどこまで書けるか試してみましょう！
その枠組みとして、計算が有限回で終わることが確実に見て取れるようなメタレベルの「原始再帰関数」について、それを対象レベルでシミュレートするような関数を考え、対象レベルにおいてもその値がメタレベルにおける計算と等しくなる（数値的表現可能性）を紹介し、その例として「2+2=4」となることをQにおいて形式的に証明してみましょう。

授業内容

1. 前回の復習
2. 1≠2
3. 計算（原始再帰的関数）
4. 証明（数値的表現可能性）
5. 成績および今後の予定

注意

1. 本来は、0だけでなく、形式化された算術の全ての記号（=,+,×など）も、本来の算数の記号と分けて書く必要があるのですが、スライド作成の都合上、同じ記号を使っています。ご注意下さい。