Catbus

This study of meta-mathematics, of proofs and propositions as objects in themselves,  was started off by David Hilbert, and revolves around the question of “what can be proven?” This is the notion of consistency- we explore Gentzen’s neat trick of cut-elimination and provide a formal proof of the consistency of Peano arithmetic.