# 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.

# Contents

## Genus of a proof

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

$x_B \to x_C$

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

$x_A \to x_C$

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

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

## References

• 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.