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 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 , 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. (shrink)

Buss, S.R., The undecidability of k-provability, Annals of Pure and Applied Logic 53 75-102. The k-provability problem is, given a first-order formula ø and an integer k, to determine if ø has a proof consisting of k or fewer lines. This paper shows that the k-provability problem for the sequent calculus is undecidable. Indeed, for every r.e. set X there is a formula ø and an integer k such that for all n,ø has a proof of k sequents if and (...) only if n ε X. (shrink)

This paper develops a proof theory for logical forms of proofs in the case of monadic languages. Among the consequences are different kinds of generalization of proofs in various schematic proof systems. The results use suitable relations between logical properties of partial proof data and algebraic properties of corresponding sets of linear diophantine equations.