We develop a combinatorial model to study the evolution of graphs underlying proofs during the process of cut elimination. Proofs are two-dimensional objects and differences in the behavior of their cut elimination can often be accounted for by differences in their two-dimensional structure. Our purpose is to determine geometrical conditions on the graphs of proofs to explain the expansion of the size of proofs after cut elimination. We will be concerned with exponential expansion and we give upper and lower bounds (...) which depend on the geometry of the graphs. The lower bound is computed passing through the notion of universal covering for directed graphs. In this paper we present ground material for the study of cut elimination and structure of proofs in purely combinatorial terms. We develop a theory of duplication for directed graphs and derive results on graphs of proofs as corollaries. (shrink)

Many times in mathematics there is a natural dichotomy betweendescribing some object from the inside and from the outside. Imaginealgebraic varieties for instance; they can be described from theoutside as solution sets of polynomial equations, but one can also tryto understand how it is for actual points to move around inside them,perhaps to parameterize them in some way. The concept of formalproofs has the interesting feature that it provides opportunities forboth perspectives. The inner perspective has been largely overlooked,but in fact (...) lengths of proofs lead to new ways to measure informationcontent of mathematical objects. The disparity between minimallengths of proofs with and without ``lemmas'' provides an indicationof internal symmetry of mathematical objects and their descriptions.A principal observation of this paper is that mathematicalstructures can be embedded into spaces of logical formulae and inheritadditional structure from proofs. We shall look at finitely-generatedgroups, rational numbers and SL(2,Z), and examples fromtopology and analysis. (shrink)

The logical flow graphs of sequent calculus proofs might contain oriented cycles. For the predicate calculus the elimination of cycles might be non-elementary and this was shown in [Car96]. For the propositional calculus, we prove that if a proof of k lines contains n cycles then there exists an acyclic proof with O(k n+l ) lines. In particular, there is a polynomial time algorithm which eliminates cycles from a proof. These results are motivated by the search for general methods on (...) proving lower bounds on proof size and by the design of more efficient heuristic algorithms for proof search. (shrink)