The Kreisel length-of-proof problem

A first-order system F has theKreisel length-of-proof property if the following statement is true for all formulas(x): If there is ak1 such that for alln0 there is a proof of(¯n) in F with at mostk lines, then there is a proof of x(x) in F. We consider this property for Parikh systems, which are first-order axiomatic systems that contain a finite number of axiom schemata (including individual axioms) and a finite number of rules of inference. We prove that any usual Parikh system formulation of Peano arithmetic has the Kreisel length-of-proof property if the underlying logic of the system is formulated without a schema for universal instantiation in either one of two ways. (In one way, the formula to be instantiated is built up in steps, and in the other way, the term to be substituted is built up in steps.) Our method of proof uses techniques and ideas from unification theory.