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.