Length of Proofs and Unification Theory Ph.D. Thesis William M. Farmer 1984 Abstract In this thesis we investigate certain questions concerning the length of proofs in formal systems, where length of proof means number of lines. We are particularly interested in trying to solve the following two open problems in proof theory: (1) The k-Provability Problem: Let k be an integer >= 1 and let P be a first-order proof system. Find a procedure to decide, given a formula phi in P, whether or not there is a proof of phi in P with length <= k. (2) The Kreisel Length-of-Proof Problem: Let P be a first-order formalization of arithmetic. Determine whether or not the following statement is true for all formulas phi(x) in P: forall x phi(x) is provable in P if and only if there is an integer k >= 1 such that, for each instance phi(n) of phi(x), there is a proof of phi(n) in P with length <= k. Using unification theory, we develop a general method of attacking these two problems for first-order proof systems that possess only a finite number of axiom schemata and rules of inference. The method centers around reducing the k-provability problem for such systems to a certain kind of second-order unification problem. (Second-order unification is involved (as opposed to first-order unification) because first-order proof systems use schemata that contain second-order variables). By solving various subproblems of this unification problem, we solve the k-provability and Kreisel length-of-proof problems for a variety of first-order proof systems, including a formalization of Peano arithmetic based on a system due to A. Tarski. In addition to our proof-theoretic results, we obtain a number of second-order unification results. In particular, we construct an algorithm for the unification of second-order monadic terms as well as show that the problem becomes undecidable upon the addition of a single binary constant, even when no function variables with arity >= 2 are allowed.