Structural Proof Theory and the Logic of Proofs
The Logic of Proofs was developed by S. Artemov in the nineties in order to solve a problem posed by K. Gödel in the thirties. It is based on the notion of a so-called "proof polynomial", which allows to talk about proofs inside of the logical language. Because of that it has found numerous applications in the areas of epistemic logic, verification systems and foundations of functional programming languages. Epistemic logic is the study of knowledge. Here the Logic of Proofs allows to reason not only about knowledge, but also about the evidence from which we obtain the knowledge. Verification is used ensure the correctness of computational systems. Here the Logic of Proofs allows to reason about the correctness of the verifier itself. The Logic of Proofs also led to foundations of functional programming languages in which the execution itself can be part of the program, in a certain sense.
Even though the field has been growing rapidly, there still are areas which are not well understood. In particular, it is not known how to design proof polynomials for logics with so-called "fixed points". This is unfortunate, because this includes important logics such as epistemic logics with common knowledge and various temporal logics. Common knowledge is a central concept in epistemic logic. It describes the fact that not only everybody knows a fact, but also everybody knows that everybody knows this fact, and everybody knows that everybody knows that... and so on. That we should go at a green light and stop at a red light, for example, is common knowledge among car drivers. Temporal logics, on the other hand, can reason about time and are central in the verification of the correctness of computational systems.
The lack of proof polynomials for fixed points in particular means that there is no formal setting in which evidence-based knowledge and common knowledge can be studied together. Also, there is no evidence-based formal setting for reasoning about time. This is the first problem we want to attack.
Also, the relationship between proof polynomials and the so-called cut elimination is not well understood. Cut elimination is arguably the most important operation on proofs. Crudely speaking it transforms a short creative proof into one that is long and not creative. Among many other things this ensures that a proofs can be found even without creativity, such as by a computer. The study of cut elimination in the presence of proof polynomials is the second problem we want to attack.
