Logical complexity and term structure

In mathematics we routinely speak and write about a large variety of different objects, often of a highly abstract nature, like infinite sets, real numbers, real-valued functions, operators transforming such functions, and so on. However, we do so in an inherently finite way: every definition, every proof, and every mathematical text is a finite sequence of symbols, taken from some finite set. As infinite and abstract the objects of our discourse may be, what we say and prove about them is thus inherently finite. This simple but striking insight lies at the root of the development of mathematical logic at the beginning of the 20th century which has revolutionised our understanding of the foundations of mathematics. This project inscribes itself into this tradition by using mathematical methods for the analysis of the language of mathematics. It sets out to broaden this methodology by extending the mathematical techniques available to such analyses and it intends to apply these newly developed techniques for obtaining new insights into the foundations of mathematics and the philosophy of mathematical practice. The topic of this project is the analysis of the structure of formal proofs, and more specifically, the role of the structure of first-order terms in proofs and their interaction with the logical complexity of formulas. The new techniques that this project will bring to fruition in proof theory and the foundations of mathematics come from automata theory and descriptional complexity. By proving a structure theorem we will show how to assign to every proof with cuts a formal tree grammar that represents the structure of the proof in a concise and logic-free way. The significance of such a result lies in the fact that, not only do we obtain a new representation of Herbrand expansions, we obtain a representation that is conceptually simple, yet at the same time closely related in structure as well as in size to the complex original proof thus providing an ideal abstraction for the analysis of the first- order layer of proofs. This makes it possible to develop both, theoretical results as well as algorithms that work on this new representation. The full-fledged development of these innovative techniques is the key to attacking deep questions about the foundations of mathematics and the philosophy of mathematical practice such as: What is the relationship between abstract proofs and concrete computations? What is the role of implicit information in definitions? Why do we prefer functional notation over alternatives? Are there complexity-theoretic reasons for the use of concepts in proofs?