証明論は、下記の 菊池 誠先生や
新井パパ PDFが、参考になるだろう

(参考)
https://www2.kobe-u.ac.jp/~mkikuchi/
菊池 誠
神戸大学 大学院システム情報学研究科 教授
https://www2.kobe-u.ac.jp/~mkikuchi/ss2018.html
数学基礎論サマースクール2018
証明論　特に算術の無矛盾性証明
不完全性定理によりペアノ算術 PA の無矛盾性は厳密には有限的に証明できないが，
ゲンツェンは順序数 ε_0 までの超限帰納法を用いて，
カット消去法によって PA の無矛盾性を，ある意味で有限的に証明した．
その後，アッカーマンはヒルベルトの ε 計算を用いた PA の無矛盾性の証明を，
ゲーデルは直観主義算術を介した PA の無矛盾性の証明を与えている．
証明論の古典とでも呼ぶべきこの三つの無矛盾性証明は，
互いに深く関係しながらも全く異なる発想のもとで同じ目的を達成する興味深いもので，
技術的にも現在の証明論や理論計算機科学の基礎となる重要なものでもある．
今回の数学基礎論サマースクールではこの三つの無矛盾性の証明と，
この三つの無矛盾性証明から始まる証明論の発展を紹介する．
2018年9月3日から6日，神戸大学
（入門・予備知識）
菊池誠：チュートリアル，趣旨説明，予備知識 [pdf1, pdf2]
https://www2.kobe-u.ac.jp/~mkikuchi/ss2018files/kikuchi1.pdf
数学基礎論サマースクール2018
証明論，特に算術の無矛盾性証明１．
導入・三つの体系
2018年9月3日 神戸大学 菊池誠
https://www2.kobe-u.ac.jp/~mkikuchi/ss2018files/kikuchi2.pdf
数学基礎論サマースクール2018
証明論，特に算術の無矛盾性証明２．
ペアノ算術・!0・ゲンツェン
2018年9月3日 神戸大学 菊池誠

（発展）
https://www2.kobe-u.ac.jp/~mkikuchi/ss2018files/50yearsPTsldshw.pdf
新井敏康：ゲンツェンから始まる証明論50年 [pdf]
（新井パパ）
https://ja.wikipedia.org/wiki/%E6%96%B0%E4%BA%95%E6%95%8F%E5%BA%B7
新井 敏康（あらい としやす、1958年 - ）は、日本の数学者・論理学者。東京大学名誉教授、千葉大学名誉教授。専門は数学基礎論[1]。国立情報学研究所教授の新井紀子は妻[2]。
2019年（平成31年）- 2024年（令和6年） - 東京大学大学院数理科学研究科教授。
（新井ママ）
https://ja.wikipedia.org/wiki/%E6%96%B0%E4%BA%95%E7%B4%80%E5%AD%90
新井 紀子（あらい のりこ、1962年10月22日[1] – ）は、日本の数学者。専門は数理論理学、教育工学、人工知能など。国立情報学研究所社会共有知研究センター長・教授。
イリノイ大学大学院在学中に数学者の新井敏康と結婚。1990年に帰国し、長女の出産