Topologic

One recent goal of proof theory is to construct invariants of proofs. What do we mean by this? Well, say we have some formal system, F, which encodes a piece of mathematics. Suppose that we have some informal proof P in this piece of maths. Now, given that F encodes the relevant piece of maths, it can encode P. However, there is very likely to be a lot of different ways of encoding P in F. For instance, we could permute non-interacting sub-proofs, change the names of variables, include sub-proofs which don't essentially do anything etc. So, we have something like a fibration going on here. That is, we can imagine a set of all informal proofs, Inf, a set of all formal proofs, For and a projection p:For → Inf. What we would like to do is to slap a system of invariants on For in such a way that two formal proofs have the same invariant if and only if they are in the same fiber. Now, one might argue that we should be using categories instead of sets, since different proofs may be related (for instance, one may be a subproof of the other). This is the basic idea behind coherence theory and we won't be getting into that today.

Anyway, what is a good way of attaching invariants to proofs? Our choices are actually severely limited and most of them use some form of proof net or another. Proof nets were introduced in Girard's 1987 paper on linear logic, though a similar idea was present in earlier work of Chomsky, under the name of "phrase markers" (these appear in "The logical structure of linguistic theory"). The basic idea behind a proof net is to take a formal proof and turn it into a directed graph. I don't have any decent drawing software on this computer, so you're going to have to use your imagination here. Intuitively, we can see why this may work. For instance, a proof in the sequent calculus is almost-always a tree (although you can use "dag-style" proofs if you prefer, where "dag" stands for directed acyclic graph. Australian readers will no doubt be amused by the oxymoronic name "dag-style"). Now, suppose that we were to look at the tree defined by some proof, S, in the sequent calculus. Suppose that we label the nodes by the inference rule used at the relevant step in the proof. Now, if we have another proof that does all the same stuff but in a different order, it is going to generate an isomorphic tree. This is, in fact, not quite how proof nets work, but it is a useful way of conceptualising things (the complications arise, for instance, from axioms, which break the tree property).

Now, those of you with a penchant for topology may well be thinking that there should be a way to obtain an invariant from a topological structure. As it turns out, several people have thought about this and come up with some neat ideas.

As a first pass, notice that proof nets are abstract graphs. But we know that we can embed graphs in topological spaces. What sorts of spaces? Well, that depends on how commutative things are. If the logic is noncommutative (nonsymmetric monoidal category), then the corresponding proof nets are planar, so we can embed them in a sphere (oh, joy!).

The problems come in when we have some amount of symmetry, or commutativity. This breaks the planarity of the graph. One might think that every time you commute two elements, you need to attach a handle to your space. This intuition is roughly correct.

Anyway, now that I have whet your appetite, let me point you to some neat papers that deal with these ideas. First up, we have:

Planar and braided proof-nets for multiplicative linear logic with Mix; G. Bellin and A. Fleury

The above paper obtains a representation of proof nets in terms of CW-complexes in a two dimensional disk. The next paper looks at proofs as two-dimensional surfaces with boundary and contains an analysis of how commuting elements affects the topology of the corrsponding surface.

Implicit exchange in multiplicative proof nets; François Métayer

This next paper goes on to show that the surface associated to the proof structure is the surface of minimal complexity on which the proof can be drawn without crossings, while respecting the local orientation:

Two-dimensional proof structures and the exchange rule; Christophe Gaubert

Finally, building on this work, this next paper transforms the topological ideas into a logical framework:

Permutative logic; Jean-Marc Andreoli, Gabriele Pulciniand Paul Ruet

There's lots of fun ideas in the above papers, so happy reading!