Lectures in Proof Theory and Complexity
These lecture notes constitute an excerpt of the contents of the course ‘Formal Systems’ taught by me for the master’s degree course ‘Applied Mathematics’ and partly for the ’Language and Mind’ master’s degree course at the University of Siena, so it was created with an educational purpose, albeit for second-level courses. They are mainly oriented towards applications of Proof Theory (one of the macro-areas into which Mathematical Logic is divided) to Computability Theory and Computational Complexity Theory, albeit with inevitable entanglements with Model Theory and with Category Theory. Preliminary, I focus on some classical results concerning formal arithmetic, dating back to the classical era of the 1930s and 1940s, then in subsequent chapters inviting a comparison with more recent results. In this regard, I strongly emphasise the acceleration imparted also to logical study by the development of computer science: in addition to decidability in principle, indeed, computer science has forced attention to be paid to the classification of mathematical problems according to their degree of difficulty and the computational means that can be used in practice. I share the view that sees a continuity with Hilbertian foundational research, i.e. his finitism, or more broadly the various trends of the constructive mathematics (i.e. which requires a more explicit characterisation of proofs than classical mathematics) and these most recent developments which led to a narrower form of finitism, although only a few so-called ’ultraintuitionists’ such as van Dantzig, Mannoury or Yessenin-Volpin had previously gone indeed so far as to consider exponentiation problematic before the contributions, between the 70s and the 80s, notably by Rohit Parikh and Edward Nelson. These led to the creation of the research area of Bounded Arithmetic and to the discovery of important connections to Computational Complexity. Central has become the (unsolved) question of whether P = NP, already formulated in nuce in the 1950s independently by Kurt Gödel and John Nash. Lastly, I outline some (in my opinion) relevant developments in the approach to classical problems such as incompleteness, that have provided a bridge to other areas of science beyond Mathematical Logic, as the emergence of the phenomenon of incompleteness in specifically mathematical (and not metamathematical) contexts, and in the field of information theory and algorithmic randomness. Far from thinking that this would be an exhaustive introduction, I also devote space to the deep connections between constructive (intuitionistic) logic, type theory (i.e. programming) and that great unifying theory of mathematics constituted by Category Theory. For reasons of space, I have not been able to go into all the topics in depth, but each chapter contains extensive bibliographical references and suggestions for independent study. The text could not be entirely self-contained and presupposes a certain familiarity with the first-order logic.