A Unification-Theoretic Method for Investigating the k-Provability
Problem

William M. Farmer

1991

Abstract

The k-provability problem for an axiomatic system A is to determine,
given an integer k >= 1 and a formula phi in the language of A,
whether or not there is a proof of phi in A containing at most k
lines.  In this paper we develop a unification-theoretic method for
investigating the k-provability problem 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 show that the k-provability problem for a Parikh system
reduces to a unification problem that is essentially the unification
problem for second-order terms.  By solving various subproblems of
this unification problem (which is itself undecidable), we solve the
k-provability problem for a variety of Parikh systems, including
several formulations of Peano arithmetic.  Our method of investigating
the k-provability problem employs algorithms that compute and
characterize unifiers.  We give examples of how these algorithms can
be used to solve complexity problems other than the k-provability
problem.