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.