A significant part of the course will be devoted to the so called "limitative results" in mathematical logic and foundations, such as the insolubility of Entscheidungsproble, and the interpretations of Goedel's first and second theorem. In this framework we will try to focus on the concept of finite and constructive mathematics. It will be necessary a premise on the main computing models, however, since the recursive partial functions and the Turing machines topics widely dealt with in other courses, we will primarily focus on lambda computation, that its inventor, Church, defined:" a set of postulates for the Foundation of Logic".
Type free lambda calcul 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 insolubility 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. 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.