Carbone on the Genus of Proofs

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.

Logic (and Other Fun Stuff) on BBC Radio 4

The BBC 4 radio program “In Our Time,” presented by Melvyn Bragg, has archives of previous features on a range of topics, including some relevant to logic. Haven’t had the time to listen to them, but it you do, let me know what you think. Might be the kind of thing you can tell your relatives to listen to when they want to know what you are interested in.

HT: Chris Green

New Open Access Logic Books from the ASL

Exciting developments! The Association of Symbolic Logic has made the now-out of print volumes in the Lecture Notes in Logic (vols. 1-12) and Perspectives in Mathematical Logic (vols. 1-12) open-access through Project Euclid. This includes classics like

I’m especially excited about the Hájek/Pudlák and Barwise/Feferman volumes, which are chock-full of useful material! Check out the full list of volumes available (click on the “Series Contents” link on the right side). For now it’s available in nicely scanned and OCR’d PDF format, perhaps there will also be a print-on-demand way of getting a bound copy.