Modern perspectives in Proof Theory

Can you briefly explain what you mean by Proof Theory?

In a way, Proof Theory is the study of mathematics, itself making use of mathematical tools. When we want to learn new things in mathematics, we gather the facts we already know and then use these to deduce – or prove – new facts. This means that the limits of mathematics are delineated by two parameters: the rules that let us conclude new things from what we know, and the theories which dictate what we are allowed to know from the beginning. A theory is just a collection of axioms: these are the sentences which are simply taken as true in mathematics and are not – or cannot be – proved.

What are the goals in Proof Theory?

We know since the 1930s that there cannot be a “master” mathematical theory. All mathematical theories are incomplete and lead to undecidable sentences which can neither be proved nor disproved. We would like to have a better understanding of which mathematical problems can be solved by which theories and which cannot, and to formulate new theories which are reasonable and useful for such problems. In Proof Theory one is often interested in characterising the consequences of various theories, and in particular in determining whether any contradictions are among these consequences.

Tell us about the idea behind this theme issue and how it came about.

By the standards of mathematics, Proof Theory is relatively young – it was born last century! In the last few years, the field has been undergoing fast changes and gaining momentum in various directions, and we wanted to compile a series of perspectives and viewpoints on its future during this crucial period. I think that this momentum will continue and the field will look very different ten years from now, but the ideas underlying this issue will still be palpable. You can read the full issue here. 

What's the biggest take-away message from the papers in the issue?

Over the last few years, Proof Theory has been slowly challenging many of its former dogmas. Without going into too much detail, this has led to the study of various aspects of mathematical theories in a more general sense, to identifying the logical content of various theorems from analysis and combinatorics, and to interactions between constructive and non-constructive aspects of mathematics. All of the papers in the issue exhibit an idea along one or more of these three lines. I think the take-away message should be: scientific traditions are there for a reason, but it’s good to be wary of them.

How was your experience of being a Guest Editor on Phil Trans A?

It was thrilling! I think that Phil Trans A is the perfect venue for what we wanted to accomplish with this issue, and the editorial and production team were very helpful all throughout the process.

Tell us a bit about your own research.

In Proof Theory, I am interested in quantifying the strength of mathematical theories and characterising their consequences, especially those of higher complexity. Outside of Proof Theory, I also work in Set Theory – which is the mathematical study of infinity – and in Computability Theory. Even when studying theories about simple objects, such as the natural numbers, the truth or falsity of high-complexity problems is influenced by the possible existence of very large infinite mathematical objects, and the consequences these may have on the properties of generalised forms of computability. My research aims at studying precisely these interactions between these three fields.

What is the future for research in Proof Theory?

Proof Theory is very young and has a bright and long future ahead. In it, we will be able to analyse more powerful mathematical theories and better understand which problems are unsolvable with our current mathematical axioms. It will also expand its degree of interaction with other areas of mathematical logic, and of mathematics in general. The better we understand the current limits of our mathematical toolbox, the easier it becomes to identify which tools are missing!

Can you say something about the cover image?

I’m glad you asked! Mathematicians are very fond of metaphors and often draw inspiration from nature when naming mathematical concepts. “Trees” are a particular kind of graph; “hydras” are a particular kind of terminating sequence of natural numbers; and “worms” are iterated consistency assertions. Each of these notions is the protagonist of a famous theorem which is known to be unprovable in first-order number theory; namely: Kruskal’s theorem, Goodstein’s theorem, and the well foundedness of the order ε₀. The cover image is an AI’s depiction of these theorems. You can also see the AI’s depiction of Hilbert’s hotel to the right, and a pullback diagram.

To read more content from Philosophical Transactions A, or to find out how you can become a Guest Editor for the journal, please visit our website.