Reasoning occurs in many domains: in academic disciplines such as physics, mathematics or history, in the courtroom, in diagnosing patients, in a debate, and so on. With the rise of the computer over the last decades, the need to automate these forms of reasoning has increased considerably. The first step in the automation of reasoning is usually to model it as a logic, and this has resulted in a great variety of logics, such as the temporal logics used in software verification; the epistemic logics in artificial intelligence and the modal logics used in medical expert systems.

To study, use and apply logics, proof systems are a popular and powerful tool. A proof system consists of axioms and rules such that statements derivable in it are exactly those statements that are valid in the logic. It thus is a syntactic description of the logic. The oldest and most well known example of a proof system is the one for geometry in Euclid’s Elements, from more than two thousand years ago.

Most logics have infinitely many proof systems, but not all of them are useful. What is useful depends on the context in which the logic is used. If the logic forms the basis for diagnostic medical software, then efficient proof systems are preferred over nonefficient ones, while if the aim is to faithfully represent epistemic reasoning, it is important that the proof system has sufficient expressive power.

Finding optimal proof systems for a logic in a given context has considerable theoretical and practical implications, as in the examples above, where it results in optimal software for diagnostic reasoning and provides means to prove facts about epistemic reasoning, for example that certain epistemic assumptions, when combined, are inconsistent.

The aim of this project is to establish what the optimal proof systems of a logic in a given setting are. The project consists of three subprojects, two in mathematical logic, one in philosophical logic. The first two develop methods to describe all possible proof systems of logics and the third one formulates a philosophical theory of formalisation. Combined they provide the mathematical and philosophical tools to reach the goals of the project.

The project is unique in that it provides the first exhaustive mathematical and philosophical account of optimal formalisation. Moreover, it has many theoretical applications in logic and several applications elsewhere.