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.

No additional funding sources recorded.