The job of a mathematician is to prove theorems - that is, to provide a rigorous, logical argument that establishes that a mathematical statement is true. If the proof is correct, then we can be certain that the theorem is true. But how can we be certain that a proof is correct?
Proof assistants are computer programs that help the user to formalise a mathematical proof, and check that the proof is correct.
They are slowly becoming important for research mathematicians. They have also become very important in the computing industries, for software verification and hardware verification: a formal proof that a product has the properties it is supposed to have, checked by a proof assistant, allows a high degree of confidence in the product.
When designing a proof assistant, one must first choose a system of logic. A system of logic consists of a symbolic language in which theorems and proofs may be written, together with a set of rules for deciding which proofs are correct. The systems of logic known as type theories have proven very successful for use in proof assistants.
Given a system of logic, we may ask: which proofs can be formalised in this system? Proofs are divided into "constructive proofs" and "classical proofs". Most computer scientists, and the vast majority of mathematicians, accept classical proofs. But proof assistants based on type theory have, so far, only been able to formalise constructive proofs; and this is quite a large constraint on their usefulness.
Certain objects, called control operators, may be added to a type theory. When these are added to some simple type theories, the theories now accept classical proofs; this is a very surprising fact, and still not well understood. However, when control operators are added in the same way to more complex type theories (dependent type theories), the theories become inconsistent; that is, it is now possible to "prove" statements that are false.
The problem is that there are several different ways in which control operators may be added to a complex type theory; we have several choices as to where we allow a control operator to appear, and how control operators interact with the other features of a type theory. The naive choice - allow them everywhere, and allow all possible forms of interaction - leads to inconsistency. Of the many other possibilities, it is not at all obvious which will be most likely to be fruitful; and investigating their properties one by one would be very time consuming.
Systems of logic known as logic-enriched type theories, or LTTs, have also been developed. These are closely related to type theories. They differ in being divided rigidly into two parts: one part - the type-theoretic component - for defining mathematical objects and programs, and one part - the logical component - for stating and proving theorems about the object. We can change the logical part to make it accept classical proofs, without changing the type-theoretic part.
However, LTTs are still quite new, and their theoretical properties and suitability for use in a proof assistant is not yet well understood.
I believe that work on control operators and work on LTTs can help each other. If we investigate the properties of type theories and classical LTTs, and translations between the two, then we should be able to reuse results and use the insights from one to shed light on the other. In particular, we should find the best way to add control operators to a complex type theory, by choosing the way that makes translation to and from LTTs easiest.
I therefore propose to construct several type theories with control operators and several classical LTTs, investigate their theoretical properties and translations between them, and experiment with their use in practice. My aim is to produce one or more systems of logic that keeps all the advantages of type theories; accepts classical proofs; and is practicable for use in a proof assistan
|