On Formalization of Model-Theoretic Proofs of Gödel's Theorems
Makoto Kikuchi, Kazuyuki Tanaka · Notre Dame Journal of Formal Logic · 1994
Within a weak subsystem of second-order arithmetic $WKL_{0}$, that is $\Pi^0_2$-conservative over $PRA$, we reformulate Kreisel's proof of the Second Incompleteness Theorem and Boolos' proof of the First Incompleteness Theorem.