Unifying structural proof theory via bounded sequent calculi

A mathematical formalisation of a system of reasoning is called a logic. Logic plays a prominent role in numerous areas of computer science, mathematical logic, linguistics, philosophy and further afield. Aside from the diversity of these domains, the reasoning that applies in these scenarios is also distinctive. No single logic applies to all these scenarios. Several prominent questions arise when investigating a logic. For example: can we efficiently determine if a given statement (reasoning) is a consequence of the logic? What is the complexity of such an algorithm? How does the logic relate to other logics in the vicinity? Proof systems are useful to answer such questions. They are mathematical formalisms that can generate (in an abstract sense) the proofs of exactly those statements that are consequences of the logic. In 1935, Gerhard Gentzen introduced an elegant proof system called the "sequent calculus" for several prominent logics, where the proof system satisfied the "analyticity" property. Roughly speaking, analyticity asserts that a proof of a complex statement is composable from proofs of simpler statements, and through this, relates the complexity of a statement to the structure of its proof. Unfortunately, it is difficult or even impossible to construct a sequent calculus with the analyticity property for most logics of interest. For this reason, the state of the art has focussed on the development of intricate new proof systems---replacing the sequent calculus. There is a price to pay: despite satisfying analyticity, due to their intricacy, it is difficult to apply these proof systems to investigate logical questions. This project aims to investigate how the intricate proof systems with analyticity could be reduced to sequent calculi satisfying various properties that are weaker than analyticity (yet still useful). Such proof systems are called "bounded sequent calculi". This project will commence a research programme on the theory of bounded sequent calculi, and will use the bounded sequent calculi to study logical questions. Ultimately, we will investigate how bounded sequent calculi could serve as a unifying mathematical formalism for the construction of proof systems and the investigation of logics.

This project developed a new and simpler way to analyse complex systems of reasoning used in computer science and related fields. Its main achievements were threefold: it introduced a unified proof framework for many different logics, obtained new results on how difficult these reasoning problems are, and provided initial tools for automating such reasoning. The project showed that many non-classical logics---used, for example, to model reasoning about resources such as time, memory, or information---can be studied within a single, simpler framework. Instead of designing a different specialised method for each logic, the project demonstrated that it is possible to harness the standard and well-understood method (the sequent calculus) and allow only carefully controlled additional steps. These new systems were called bounded sequent calculi. A key innovation was to rethink how these additional steps are handled. Traditionally, researchers tried to eliminate them entirely, but this is often impossible for important logics. The project instead showed that allowing such steps in a restricted way preserves much of the usefulness of the system while greatly increasing its applicability. This made it possible to recover, within a single framework, the essential insights of many previously developed and more complicated methods. In doing so, the project addressed a longstanding issue in the field: the proliferation of many overlapping and difficult-to-compare proof systems. The new approach provides a common basis for understanding and comparing them. A second major achievement was the development of new methods for analysing the difficulty of reasoning in these systems. The project introduced techniques based on well-quasi-orderings, which ensure that certain computational processes must eventually terminate. Using these methods, it established new results on whether reasoning problems can be solved at all (decidability) and how complex they are. A notable example is the fundamental fuzzy logic MTL, for which the first meaningful upper bound on its complexity was obtained, resolving a long-standing open problem. At the end of the project, this bound was significantly improved even further. The project also explored practical aspects by developing a prototype implementation of these methods as automated reasoning tools. Such tools are important for applications like software verification, where one needs to check that systems behave correctly. Finally, the project extended the classical algorithm from the 1930s for eliminating cut-rules from sequent calculi to this new setting. This was achieved for several important cases, with the general theory forming the basis for ongoing work. Overall, the project provides a unified understanding of complex reasoning systems, with new results on their computational complexity and progress towards automated theorem proving.