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

I introduce the falsifier calculus, a new deep-inference proof system for first-order predicate logic in the language of Hilbert's epsiloncalculus. It uses a new inference rule, the falsifier rule, to introduce epsilon-terms into a proof, distinct from the critical axioms of the traditional epsilon-calculus. The falsifier rule is a generalisation of one of the quantifier-shifts, inference rules for shifting quantifiers inside and outside of formulae. Like the epsilon-calculus and proof systems which include quantifier-shifts, the falsifier calculus admits non-elementarily shorter cut-free proofs of certain first-order theorems than the sequent calculus.

Analogous to the way in which Herbrand's Theorem decomposes a proof into a first-order and a propositional part, connected by a Herbrand disjunction as an intermediate formula, I prove a decomposition theorem for the falsifier calculus which gives rise to a new notion of intermediate formula in the epsilon-calculus, falsifier disjunctions. I then prove that certain first-order theorems admit non-elementarily smaller falsifier disjunctions than Herbrand disjunctions.