University of Calgary

# Complexity measures of proofs

## This website has moved!

You are looking at an archived page. The website has moved to richardzach.org.

Submitted by Richard Zach on Fri, 03/18/2005 - 7:04pm

In the last post, I pointed to some interesting work on cut-elimination and complexity of proofs. This reminded me of Richard Statman's wonderful dissertation (Structural complexity of proofs, Ph.D. thesis, Stanford University, 1974). The two most widely investigated measures of proof complexity are size (number of symbols) and length (number of steps). Statman and Orevkov's speedup results for sequent calculus concern length. In one chapter of the thesis, Statman considers another measure, which applies to proofs in natural deduction: Consider a proof tree in natural deduction, this gives you a graph (inferences are nodes, edges connect two inferences if the premise of one is the conclusion of the other). Now also connect each assumption in the proof (leaves of this tree) with the inference at which it is discharged. This, in contrast to the plain proof tree just considered, is no longer a planar graph: some edges cross. So you can now consider the genus of the resulting graph as a complexity measure: the minimum number of handles on the sphere so that you can embed the graph without edges crossing. Statman showed that normal proofs have superexponential speedup over non-normal proofs with respect to the genus measure. (Unfortunately, Statman never published this, to the best of my knowledge. My copy is back home and I unfortunately can't check the details.) There is some related recent work on geometric considerations in proof complexity, e.g., Girard's proof nets and the logical flow graphs considered by Buss and Carbone. Now I just found a recent PhD thesis by Anjolina Grisi de Oliveira which looks at these things. (See also this paper.) Would be nice if I had time to read it; maybe someone else does and wants to let me know what's in it.