nLab Structural Complexity of Proofs

Structural Complexity of Proofs (1974) is the title of a Ph.D. thesis by Richard Statman, who was a student of Georg Kreisel at Stanford University. Among other contributions, the thesis is notable for defining a notion of “genus of a proof”, as a global measure of complexity more interesting than (but analogous to) number of inferences, depth of the proof tree, etc.


Genus of a proof

Any proof π\pi in natural deduction induces a rooted tree, by representing the judgments BB occurring in the proof as nodes x Bx_B (note that different occurrences of the same judgment are represented as distinct nodes), and drawing a directed edge

x Bx Cx_B \to x_C

just in case BB occurs as a premise of the inference rule with conclusion CC. This rooted tree can then be turned into a directed graph G(π)G(\pi) by adding more edges

x Ax Cx_A \to x_C

just in case the assumption AA is discharged by the inference rule with conclusion CC (see natural deduction: hypothetical reasoning?).

The genus of the proof π\pi is then defined to be the graph genus of G(π)G(\pi), i.e., the minimal genus of a surface in which G(π)G(\pi) embeds without crossing edges.


1: The Effect of the Elimination of Explicit Definitions on the Complexity of Proofs

2: The Effect of the Choice of Recursion Equations and Rules on the Lengths of Equational Proofs

3: Strong Normalization of Classical Analysis with Some Applications to the Length of Proofs


  • Richard Statman. Structural Complexity of Proofs, Ph.D. Thesis (1974), Stanford University.

  • Alessandra Carbone. Logical structures and the genus of proofs, APAL 161:2, 2009. (doi)

category: reference

Last revised on March 10, 2015 at 11:58:44. See the history of this page for a list of all contributions to it.