A significant part of the course will be devoted to the so called "limitative results" of formal systems (in a broader sense) in mathematical logic and foundations, such as the unsolvability of Entscheidungsproblem, and the interpretations of Goedel's first and second theorem, but also of the less famous Tennenbaum's result on non computability of non-standard models of arithmetic. In this framework we will try to focus on the concept of finitist and constructive mathematics. It will be necessary a premise on the main models of computation, however, since the partial recursive functions and the Turing machines topics widely dealt with in other courses, we will primarily focus on lambda calculus, that its inventor, Church, defined:" a set of postulates for the Foundation of Logic".
Type free lambda calculus is one of the great models of computation, in a precise sense equivalent to partial recursive functions and Turing machines.
Church used this tool to prove the unsolvability of the Entscheidungsproblem. In its subsequent developments and in the later versions, it was the basis for further research into the constructive foundations of mathematics and an important link between logic and functional programming. In particular Goedel's system T of arithmetic in all finite types was introduced as an extension of the finitary standpoint, to provide a consistency proof of arithmetic, but its applications went beyond the original intentions, becoming a precursor of modern approaches to type theory, until Martin-Lof intuitionistic foundation for constructive mathematics. Another goal is to introduce further advanced topics in proof theory as Gentzen's sequent calculus relevant in computability theory.The course is based on lectures prepared by the teacher. Seminars are planned, valid for the final exam, on scientific articles that will be proposed during the course.