There are interpretations of Herbrand’s theorem extending its scope to formal number theory, though at the expense of analyticity, its most desirable property. Therefore, deepening our understanding of the analyticity boundary is important to many areas of computer science, as inductive theorem proving has a wide range of applications. One approach to studying this bound is through cut-elimination and how we can transform proofs using inductive reasoning. In this talk, we discuss cut-elimination by resolution, how to extend the method to proof schema, infinite sequences of proofs, and the framework presented in “Schematic Refutations of Formula Schemata.”