Non-Elementary Compression of First-Order Proofs in Deep Inference Using Epsilon-Terms

In recent years, there has been interest in developing proof systems for first-order predicate logic which, for certain theorems, admit cut-free proofs that are non-elementarily shorter than in traditional Gentzen systems. In this talk, I will introduce the "falsifier calculus", a proof system defined in the language of Hilbert's epsilon-calculus which enjoys this non-elementary compression. Although the epsilon-calculus has its historical roots in Hilbert's program and was initially designed to establish a consistency proof for arithmetic, I shall demonstrate that expanding the language of first-order logic by epsilon-terms can yield novel normalisation results for first-order proofs and a new perspective on the non-elementary compression of cut-free proofs.