Proofs as Games

Proof theory has undergone many transformations over the hundred or so years of its existence. It seems reasonable to roughly segregate its development, though note that my partition of history is rather arbitrary! In particular, important open problems from each period are still being actively researched today and I haven't mentioned stuff like proof complexity. Nevertheless, here it is:

1. 1900-1930: The birth of proof theory, in the guise of Hilbert's program for formalising mathematics. The end of this period is marked, of course, by the incompleteness theorems. However, this is not to say that the program was completely without use. On the contrary, much current work in computer science can be seen as an extension of work arising from this period. For instance, Russell and Whitehead's Principia did not give us a foundations for mathematics, but it did so for programming language theory by giving us type theory. Moreover, Hilbert's epsilon calculus is still going strong and is in active use in the proof assistant community.
2. 1931-1986: This period predominantly consisted of analysing the ordinal strength of increasingly complex systems. A representative problem of this period was Takeuti's Conjecture, which is roughly the assertion that second order logic has cut elimination. Or, if you want to be fancy, you can say analysis instead of second order logic. This conjecture implies, for instance, the consistency of full second order arithmetic (PA2). Of course, Takeuti's conjecture cannot be proven from within PA2. As such, it was widely believed to be false for quite a while. This belief turned out to be wrong. The first proof was given by Tait in 1965, building on previous work of Schutte. This proof was semantic, a style of proving cut elimination that is often unsatisfactory since it does not provide enough information. In 1972, Jean-Yves Girard provided a syntactic proof of the theorem and subsequently gave birth to System F, which has continued to hold importance for programming language theory.
3. 1987-2000: I choose to mark the beginning of this period with Girard's paper on linear logic. This view may be somewhat contentious. The reason is that, if one focuses on the exponential-free fragment of linear logic, then these logics had been around for many years under various names (relevant, paraconsistent, substructural,...). However, the main feature of Girard's approach is more philosophical: we should study proofs as the objects of interest, not the set of provable assertions. Subsequently, our semantics should be a semantics of proofs. That is, formulae should correspond to objects in a space and proofs to maps between them. In this way, we can begin to ask what distinguishes proofs of the same assertion. Developing a good semantics of proofs is an ongoing problem and much exciting work remains to be done. Already at this stage of history, there were indications that classical proof systems such as sequent calculi would buckle under the pressure of applications. They managed to hold up, but only just...
   
4. 2001-Present: Welcome to the new millenium! With the majority of logicians finding themselves in computer science departments, proof theory has become a powerful weapon for attacking computational problems. It turns out that the world of computation presents many more challenges for proof theory than the world of truth. For instance, in a concurrent or distributed system, it matters in what order processes are executed. This leads to a whole host of concerns, since nice things like conjunction no longer commute. Moreover, computers are now networked, with computations regularly being distributed around many machines. What does interactive computation mean? What, pray tell, is a computational problem anyway and how can we capture this in logic?

Typically, for a computational logic, nobody knows how to give a cut-free sequent calculus or similar system. This has led to a host of different formalisms being invented or brought in from the cold, with the inter-relationships amongst them not completely understood: Display logic, hypersequents, calculus of structures, proof nets, cirquent calculus,...

The problem is fundamental. If we are going to take seriously the claim that proofs correspond to programs, then we need a system that facilitates the study of the dynamics of proofs. Arm-wavy claims such as "linear logic is resource sensitive" are not sufficient. Increasingly, logicians and computer scientists are starting to desire a reasonable model of interactive computation. Two related systems present themselves at the moment: Computability Logic, introduced by Giorgi Japaridze and Ludics, introduced by Girard. The striking feature of each is that they are based on the idea of modelling computations/proofs by certain games. Computability Logic presents a major problem to proof theory, since it is semantically motivated and developed, with no clear way of capturing it in a syntactic system. As for Ludics, it is not clear precisely how it relates to computation.

As I am currently teaching myself both computability logic and ludics (I spent most of the morning printing and binding imposingly heavy papers!), I have decided to make a series of posts keeping a log of my progress. If anyone else is interested in learning about these systems, let me know and we can maybe do an internet-based reading group thingy!