On formalization of model-theoretic proofs of Gödel's theorems
weak subsystem of second-order arithmetic
scientific article; zbMATH DE number 769232