■

前回、最小述語論理の存在量化子の導入・除去規則を学び、とりあえず最小述語論理の道具立ては揃いました。授業第九回目の今回は、この枠組みの中で、実際の数学の証明がどこまで書けるか試してみましょう！
その題材としては、形式化された自然数論（自然数と足し算・かけ算の世界）の一つである、最小算術 Q の断片（大小関係に関する公理を除去したもの）を選びます。