Sharpened lower bounds for cut elimination (Q2892684)

A previous lower bound for cut elimination was of the form \(2^{h(P)}_{\epsilon d}\), where \(h(P)\) is the height of the proof \(P\), \(d\) is the maximal complexity of cuts in \(P\) and \(\epsilon\sim 1/2\). The present paper establishes \(\epsilon\sim 1\). More precisely, \(\epsilon d\) is replaced by \(d-c\) where \(c\leq 8\). This is very close to the existing upper bounds for cut elimination from arbitrary proofs leaving a gap of only \(\log^*\), the inverse superexponential function. The argument in the present paper starts with short proofs with cuts (due to V. Orevkov and other authors) of the totality of \(2^n_x\) for every \(n\). Then inductive formulas are simplified in an equivalent way to lower their complexity.