On the number of steps in proofs (Q1119576)

The paper considers the following measures of complexity of proofs: length \((=the\) number of symbols in the proof), depth \((=the\) maximal depth of a formula in the proof) and number of steps \((=the\) number of formulas in the proof). Some upper bound results for first-order logics are obtained: A bound on the depth in terms of the number of steps, a bound on the depth in terms of the length, a bound on the length in terms of the number of steps (for restricted systems). Some interesting applications are given: A bound on the number of steps in a cut-free proof, bounds on the number of steps in proofs of Paris-Harrington sentences.