A unification-theoretic method for investigating the k-provability problem

The k-provability for an axiomatic system A is to determine, given an integer k ⩾ 1 and a formula ϕ in the language of A, whether or not there is a proof of ϕ 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- probability problem for a variety of Parikh systems, including several formulations of Peano arithmetic. Our method for investigating the k-provability problem employs algorithms that compute and characterize unifiers. We give some examples of how these algorithms can be used to solve complexity problems other than the k-provability problem.