 Gentzen’s consistency proofs for arithmetic  launched a field of research known as ordinal analysis, and the program of measuring the strength of mathematical theories using ordinal notations is still pursued today. This is particularly relevant to the extended Hilbert’s program, where the goal is to justify classical mathematics relative to constructive, or quasi-constructive, systems. Gentzen’s methods of cut-elimination (and extensions to infinitary logic developed by Paul Lorentzen, Petr Novikov, and Kurt Schütte) have, in large part, supplanted epsilon substitution methods in these pursuits. But epsilon calculus methods provide an alternative approach, and there is still active research on ways to extend Hilbert-Ackermann methods to stronger theories. The general pattern remains the same: