Completeness of a cut-free calculus with equality and function constants.
Completeness properties of classical theories of finite type and the normal form theorem [Book]
Connections between cuts and maximum segments
Consistency proof without transfinite induction for a formal system for turing machines.
Cut elimination for impredicative infinitary systems. Part II Ordinal analysis for iterated inductive definitions.
Cut-elimination for impredicative infinitary systems. Part I. Ordinal-analysis for ID1.