Logical structures and genus of proofs (Q1035649)

To measure the complexity of a (formal) proof, the author introduces the notion of genus. The object of investigation of this paper is classical sentential sequent calculus. The starting point is Gentzen's threads [`Faden'], which S. Buss organized as a logical flow graph. To resolve crossing-over of edges, the author embeds a graph on the surface of a sphere with handles. The genus of a proof is, of course, the minimum number of handles necessary. She shows the existence of a cut-free proof of genus \(n\), for any \(n\geq 0\). If the genera of proofs of two upper sequents of a cut are \(k\) and \(l\), respectively, then the genus of the proof with the cut is between \(k+l\) and \(k+l+ r-1\), where \(r\) is the number of atomic formulas occurring in the cut formula. Another kind of result is the realizability of any non-oriented graph as the logical flow graph of a cut-free proof. This is an unpublished result of R. Statman from the early 1970's. The author reformulates and proves it in a graph-theoretic format.