P.S. Novikov’s work in proof theory: The method of `regular formulas’

Novikov’s interests shifted to mathematical logic and foundations of mathematics. Striving to prove the consistency of foundational theories by constructive means, he invented a method of `regular formulas’ that can be seen as a form of cut-elimination in the context of infinitary logic, predating the works by Lorenzen and Schütte. We will survey this less known chapter of Novikov’s legacy.