Georg Moser and I finally got our paper done for the Studia Logica special issue on cut elimination. It’s on the complexity of the epsilon elimination procedure in the first epsilon theorem. (If you don’t know what the epsilon theorem or the epsilon calculus is, see here.) It’s a consequence of the cut-elimination theorem that if you can prove an existential sentence ∃x A(x) then you can prove a disjunction A(t₁) ∨ … ∨ A(t_n). Moreover, the length and cut-rank of the proof of ∃x A(x) gives a bound on n, which is hyperexponential. Orevkov and Statman showed that this bound is optimal. The first epsilon theorem is like the cut-elimination theorem, just for the epsilon calculus, in that it also yields the above version of (one direction of) Herbrand’s Theorem. We show that it has essentially the same upper and lower bounds. Our paper is also the only place, I believe, were you can find Bernays’ original proof of the first epsilon theorem in English.

The paper is up at arxiv.