Lower bounds for lengthening of proofs after cut-elimination

V. P. Orevkov

Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part VIII, Tome 88 (1979), pp. 137-162

Résumé

Let $C_k^*$ be the formula \begin{align} \forall b_0((\forall w_0\exists v_0 P(w_0,b_0,v_0) \\forall uvw(\exists y(P(y,b_0,u)\\exists z(P(v,y,z)\notag\\ \ P(z,y,w)))\supset P(v,u,w)))\supset\exists v_k(P(b_0,b_0,v_k)\notag\\ \\exists v_{k+1}(P(b_0,v_k,V_{k-1})\\dots\exists v_0 P(b_0,v_1,v_0)\dots))).\notag \end{align} and let $LK$ be the Gentzen system for classical predicate calculus. Given a sequent calculus $\mathfrak P$ let $\mathfrak P\vdash_nS$ mean that $S$ has a proof in $\mathfrak P$ of at most $n$, sequent occurrences. The main aim of the paper is to show that (a) there is a linear function $l$ such that $LK\vdash_{l(k)}C_k^*$, (b) there is no Kalmar elementary function $f$ with $(LK-\operatorname{cut})\vdash_{f(k)}C_k^*$. In particular $LK\vdash_{253}C_6^*$ but $\rceil C_6^*$ does not have a refutation in resolution method with less than $10^{19200}$ clauses.