Efficient and Natural Proof Systems

We are all familiar with the language of classical logic, which is normally used for both mathematical and informal arguments, but there are other important and useful logics. Some nonclassical logics, for example, can be associated with programming languages to help control the behaviour of their programs, for instance via type systems.

In order to define the proofs of a logic we need a proof system consisting of a formal language and some inference rules. We normally design proof systems following the prescriptions of some known formalism that ensures that we obtain desirable mathematical properties. In any case, we must make sure that proofs can be checked for validity with a computational effort that does not exceed certain limits. In other words, we want checking correctness to be relatively easy, also because this property facilitates the design of algorithms for the automatic discovery of proofs.

However, there is a tension between the ease by which proofs can be checked and their size. If a proof is too small, checking it is difficult. Conversely, formalisms that make it very easy to check and to search for proofs create big bureaucratic unnatural proofs. All traditional proof systems suffer to various extents from this problem, because of the rigidity of all traditional formalisms, which impose an excess of structure on proof systems.

We intend to design a formalism, provisionally called Formalism B, in which arbitrary logics can be defined and their proofs described in a way that is at the same time efficient and natural. Formalism B will ideally lie at the boundary between the class of proof systems and that of systems containing proto-proofs that are small and natural, but are too difficult to check. In other words, we want to maximise naturality by retaining as much efficiency as possible in proof representation. A driving force in this effort will be the use of existing algebraic theories that seem to capture some of the structure needed by the new formalism.

There are two main reasons for doing this. One is theoretical: the problem is compelling, and tackling it fits well into a research effort in the theory of computation that tries to define proofs as more abstract mathematical objects than just intricate pieces of syntax. Suffice to say that we are at present unable to decide by an algorithm when two seemingly different proofs of the same statement use the same ideas and so are equivalent, or not. This is a problem that dates back to Hilbert and that requires more abstract ways to describe proofs than traditional syntax provides.

The second reason is practical: we need formal proofs to verify the correctness of complex computer systems. The more powerful computer systems become, the more we need to ensure that they do what they are supposed to do. Formal verification is increasingly adopted as a viable instrument for this, but still much needs to be done in order to make it an everyday tool. We need to invent proof systems that simplify the interaction with proof assistants, and that could represent in some canonical way proofs that are essentially the same, so that no duplication occurs in the search for and storing of proofs in proof libraries.

This project intends to contribute by exploiting proof-theoretic advances of the past ten years. We have developed a new design method for proof systems that reduces the size of inference steps to their minimal terms, in a theory called `deep inference'. The finer scale of rules allows us to associate proofs with certain purely geometric objects that faithfully abstract away proof structure, and that are natural guides for the design of proof systems whose proofs would not suffer from several forms of bureaucracy.

In short, after a decade in which we broke proofs into their smallest pieces, by retaining their properties, we are now reshaping them in such a way that they still retain all the features we need but do not keep the undesirable ones.

Formal, machine checkable proofs are increasingly used in computer science to ensure the correctness of complex hardware and software systems. Formal proofs are manipulated by complex pieces of software called proof assistants. At present, the cost of formal verification is high, and this limits its use only to the most critical systems. Part of the cost is due to the complexity of using proof assistants, which in turn depends on the relative artificiality of the languages in which formal proofs are expressed. For the same reasons, formal mathematical proofs are seldom used, and most mathematics is built around informal proofs that can in principle be formalised, but in practice are not.

The naturality, or lack thereof, of proof assistants depends on the formalisms on which they are based. The current ones are due to Gentzen (1930s). In this project we intend to design new formalisms that will be intrinsically less syntactic and more natural than Gentzen formalisms. This is a similar situation to the beginnings of computer algebra, in the 1960s. Then, the problem was to devise convenient languages and algorithms for symbolic algebraic computation; now we have a similar problem for the creation and manipulation of mathematical proofs.

We expect this impact on society and economy:

1) Maintaining a strategic research position and training students and researchers (with immediate effect). Research in deep inference has seen recent investment in the order of millions in continental Europe. It is the interest of the University of Bath and of the UK to maintain a strong presence in this area and to ride this wave. This grant will help training researchers and working with European collaborators, and it will help to secure further European funds in the near future. Some of this research will be integrated into our teaching, so educating graduates with a unique set of cross-disciplinary skills related to verification.

2) More efficient and easy to use proof assistants (in 10 years). We expect that the languages and algorithms produced by our research will become integral part of the verification tools of the future. This will be a technological advance primarily benefiting industry (banking, transports, commerce, etc.) and the general public, whose security and welfare will be better guaranteed than is the case today. In addition, we will contribute to the creation of proof assistants that will be friendlier than the current ones towards working mathematicians. In fact, we hope that, in the not too distant future, mathematicians will be able to effectively interact with computers in order to create proofs. This seldom happens today, one obstacle being the artificiality of the languages employed for formal proofs.

3) Formalisation of mathematics and creation of a universal mathematics database (in 20 years). There are ongoing efforts to create a universally accessible database of mankind's mathematical knowledge. The formalism that we will design in this project will help solve the problem of the identity of proofs, which requires the discovery of a unique representation for mathematical proofs that is able to capture their structure and ideas without unnecessary details. A solution to the proof identity problem is important for the formalised mathematics database, because it would ensure that only unique representatives of proofs would be contained in it, instead of countless and meaningless variants that would hinder its use. The impact will primarily be of a technological nature on academia and the industry, with indirect benefits to the general public. In fact, the mathematics database will revolutionise mathematical research and its teaching, thus boosting all the scientific disciplines that depend on mathematics. Therefore, all kinds of new technologies that depend on scientific discoveries and that benefit everybody will be boosted (two examples among millions are new drugs and new materials discovery).