The Kreisel Length-of-Proof Problem

William M. Farmer

1992

Abstract

A first-order system F has the Kreisel length-of-proof property if the
following statement is true for all formulas phi(x): If there is a 
k >= 1 such that for all n >= 0 there is a proof of phi(S^n(0))) in F
with a most k lines, then there is proof of forall x phi(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.