A long time ago I posted on Richard Statman‘s dissertation work on the geometrical complexity of proofs: take a proof in natural deduction, interpret the formulas in it as nodes of a graph with edges going from premise to conclusion of an inference and from assumption to the (conclusion of the) inference where it is discharged. The genus of that graph is an interesting complexity measure. Ale Carbone has also worked on this complexity measure, and now has an exciting paper entitled “Logical structures and genus of proofs” forthcoming in the Annals of Pure and Applied Logic. Here’s the introduction:
The objects of our analysis are proofs. We shall not ask why we prove a statement, nor how to show a statement, but how difficult it is to prove it. An answer to the third question might give insight into the second.
At present, there is no notion that captures well how difficult it is to prove a theorem. Measures employed to grasp this idea are the number of steps and symbols used in a deduction, and these measures are far too rough: proofs containing no cuts/lemmas usually have a larger number of steps and symbols than proofs with cuts, but their combinatorial structure is simple, essentially a tree; on the other hand, the combinatorial structure of proofs with cuts can be quite intricate, and lemmas might be very hard to guess. Despite this, in practice, we look for lemmas in order to show a theorem.
Here we consider the genus of a proof as a measure of proof complexity and we discuss a few geometrical properties of logical flow graphs of proofs, with and without cuts, with the purpose of representing how complicated a cut-free proof can be. The main result of the article says that arbitrarily complicated non-oriented graphs, that is graphs of arbitrarily large genus, can be encoded in a cut-free proof. This fact was proved by Richard Statman in his thesis written in the early seventies and never published. Here, we reformulate Statman’s result in a purely graph theoretical language and give a proof of it. We show that there are several ways to embed non-oriented graphs of arbitrary complexity into cut-free proofs and provide some other direct embeddings of arbitrarily complex non-oriented graphs into proofs possibly with cuts. We also show that, given any formal circuit, we can codify it into a proof in such a way that the graph of the circuit corresponds to the logical flow graph of the encoding proof.