一階述語論理におけるカット除去定理のアルゴリズムがカルマールの意味で非初等再帰的であることは有名であるが，命題論理ではどうだろうか？実は命題論理に関しては、証明体系を工夫することにより初等再帰的なアルゴリズムを得ることができる。これから従…

順序数解析の文献について纏める．殆ど私の備忘録． 日本語で読めるもの 教科書 論文 Buchholzの-規則 作用素に統御された証明 順序数解析の概説 以降の順序数解析 日本語で読めるもの 新井敏康．数学基礎論．岩波書店．2016． しっかりと証明が書かれている…