The number of proof lines and the size of proofs in first order logic (Q1102280)

A presentation of the results uses the particular formulation of Gentzen's well-known calculus LK as defined in \textit{G. Takeuti}'s book [Proof theory (1975; Zbl 0354.02027 and Zbl 0355.02023)]. The size of a formula is the number of symbols in it. The size of a sequent is the sum of the sizes of formulas in the sequent. The size of a proof is the sum of the sizes of the sequents in the proof. The number of proof lines of the proof is the number of vertices of a corresponding rooted tree. The main question: Suppose a sequent \(\Gamma\to \Delta\) of size m has a proof with k lines in LK. How can we bound the minimal size of a proof of \(\Gamma\to \Delta\) in LK using k and m? If the sequent has a cut-free proof with k proof lines, then the paper gives an upper bound which is exponential in \(k+m\). In general only a primitive recursive bound in \(k+m\) is obtained. It is an open problem if there is a fixed time iterated exponential bound. The results are based on a reduction to the unification problem.