Master's in Mathematical Logic and Foundations of Computer Science

The preliminary course will take place from September 2 to 13.

• Propositional calculus: truth tables, tautologies, normal forms, compactness.
• Predicate calculus: first-order languages, terms, formulas, models; satisfaction of a formula in a model; substructures; isomorphisms; elementary equivalence.
• Set theory: axioms of Zermelo-Frænkel; cardinals; Cantor and Cantor-Bernstein theorems; finite sets, countable sets.
• Introduction to programming: introduction to Ocaml functional programming; connection to lambda-calculus, recursivity, ML typing; common data structures (Boolean, integers, lists, options, trees, etc.).

• 1st-order languages, structures, theories
• Ultraproducts, compactness.
• Elementary extensions, Lowenheim-Skolem theorems, elementary chains.
• Preservation theorems.
• Back-and-forth arguments.
• Quantifier elimination, model completeness
• The space of types.
• (If time allows it) Realized and omitted types, atomic models.

• Axioms of ZF
• Ordinals, cardinals, transfinite recursion
• Ordinal and cardinal arithmetic
• The Axiom of Choice and equivalents, filters and ultrafilters
• Cofinality, regular/singular cardinals, König's theorem
• Stationary and club sets, Fodor's lemma
• Absoluteness and reflection theorems
• The constructible universe

• Completeness theorem of the LK sequent calculus with equality by Henkin's witnesses.
• Sequent calculus: cut elimination of and median sequent theorem in LK. Herbrand's theorem. LJ sub-calculation: intuitionist logic and its BHK interpretation. Properties of the sub-formula and existential witnesses in LJ.
• Natural deduction: NK and NJ systems. Cut elimination in NJ. Properties of the sub-formula and existential witnesses in NJ, then in HA (intuitionist arithmetic).
• Lambda-calculus: Confluence and standardization properties. Representation of recursive functions. T system. Curry-Howard correspondence. Realizability, strong standardization and program correctness.

• Computability: recursive functions and functions computable by machines; logical characterization of computable functions; s-m-n theorem and fixed point theorems; the concept of reduction and undecidable problems.
• Introduction to complexity: time and space complexity classes, hierarchy theorems, reductions, completeness, Boolean circuits, introduction to algebraic complexity.
• Formal arithmetic: Peano axioms and weak subsystems; arithmetization of logic; undecidability theorems; Gödel's incompleteness theorems.

The course presents the fundamental concepts of category theory, accompanied by numerous examples. The main goal is to pave the way towards the modern applications of category theory in logic, theoretical computer science and homotopy theory.

This course is a natural continuation of the first semester Model Theory course. It will seek to understand and classify the models of a given 1st order theory through the types that can be realized or omitted.

From its early development, valued fields have always played an important role in model theory. One reason for this interest is that their strong connection to arithmetic and geometry has allowed the introduction of model theoretic techniques in other fields of mathematics, resulting most often in the resolution of open questions in that field.

One of the first example of such an interaction can be found in the work of Ax-Kochen and independently Ershov who gave a solution to Artin’s conjecture on the existence of solution to homogeneous equations over p-adic fields. One of the core concept of their proof is a reduction of a question on certain characteristic zero Henselian fields, in that specific case the description of its theory, to this very same question on their residue field and value group. The idea of this reduction can be found time and time again in later work on the model theory of valued fields.

The goal of this class will be, starting with questions of quantifier elimination and then moving on to Shelah’s classification theory and more « geometric » model theory, to show the ubiquity of this Ax-Kochen-Ershov principle in the model theory of valued fields. We will also try, as much as it is possible, to give an insight into some of the recent applications of the model theory of valued fields.

Set theory means many things to many people, but most will agree that it is a subject of mathematics that has two main roles: a foundational role in the way it gives axioms to most (although not all) aspects of modern mathematics, and a mathematical role in the way that it provides a firm theory of infinity. In its most common axiomatisation, Zermelo-Fraenkel with Choice (ZFC), set theory has been able to join these two roles to the point that each describes the strength and the limits of the other. These are best understood through the study of inner and outer models of set theory, notably the constructible universe L and the method of forcing.

This course will open the first pages of the advanced set theory, assuming that the student already knows basic axiomatic set theory. It will describeforcing, go through the classical proof that the Continuum Hypothesis is not a consequence of the axioms of ZFC and then continue to give some more classical forcing notions, for example the Lévy Collapse. This will naturally lead to the study of iterated forcing and Martin’s Axiom, some applications and limitations.

Large cardinal axioms postulate the existence of cardinals with a given degree of transcendence over smaller cardinals and provide a superstructure for the analysis of strong mathematical statements. The investigation of these axioms is indeed a mainstream of modern set theory. For instance, they play a crucial role in the study of definable sets of reals and their regularity properties such as Lebesgue measurability. Although formulated at various stages in the development of set theory and with different motivation, these hypotheses were found to form a linear hierarchy reaching up to the inconsistency. All known set-theoretic propositions can be gauged in this hierarchy in terms of their consistency strength, and the emerging structure of implications provides a remarkably rich, detailed and coherent picture of the strongest propositions of mathematics as embedded in set theory.

Proof theory has undergone at least two major developments over the past century as a result of Gödel's incompleteness theorems. The first took place in the 1930s, immediately after the results on incompleteness, with the introduction and study of natural deduction and sequent calculus s by Gentzen and lambda-calculus by Church. Church then showed the undecidability of predicate calculus via lambda-calculus while introducing a universal computation model while Gentzen deduced the consistency of various logical systems as a corollary of cut elimination of breaks in sequent calculus.

The second stage took place in the 1960s with the gradual highlighting, through the Curry-Howard correspondence, of the profound links between proofs and programmes, from the correspondence between simply typed lambda-calculus and minimal propositional natural deduction to the various extensions of this correspondence to the second order, to classical logic and to the emergence of the notion of linearity in proof theory. Linear logic has profoundly renewed the links between the formal semantics of programming languages on one hand and proof theory on the other. Linear algebra is the third pole of this correspondence, focusing on the notion of computational resource.

The basic course covered the first step. This course will be devoted to the developments since the 1960s and will present the classical tools for the study of the Curry-Howard correspondence. After some review and additions to the basic course, the course will focus on two fundamental concepts, the second order and linearity, and their development, particularly in an algebraic context. In particular, the results of the course will be applied to the study of PCF, an idealized programming language.

The objective of the course is to present several points of view on complexity from logic, recursion theory or analysis. The common feature of these approaches is that they move away from the notion of the machine (and its associated measures such as time and space) in favour of a more descriptive view of the calculation. The course aims in particular to study logical formalisms in terms of their power of expression and to present multiple characterizations of the usual complexity classes.

These descriptive or implicit approaches to complexity have had important applications in database theory, programming languages and more recently in the analysis of differential equation systems, or in understanding the power of alternative computational models based on bioinformatics, or analog computation.

We will first aim to present results on classical complexity [8, 13], to extend to algebraic models such as Blum Shub and Smale's model [3, 2], to continuous space such as neural network/deep learning models [17], then to time and continuous space such as Shannon's model [16].

The course take place during the last 6 weeks of the 1st semester and the first 6 weeks of the 2nd semester.

One half of this module will consist of course work, the other half will consist of practical work on a machine. The course will finish with a project to be carried out in Coq. The first part of this course is a prerequisite for the Homotopy Type Theory course.

Homotopy theory, which is devoted to the study of spaces up to deformation, has given rise to a branch of algebra called homotopical algebra, in which tools are developed for dealing with structures in which laws like associativity do not hold exactly like in classical algebra, but up to homotopy, these homotopies being themselves subject to coherences, etc.

Homotopy theory has also a logical side, in which types, proofs of equality, and proofs of equality of proofs of equality are interpreted as spaces, paths, and homotopies between paths, respectively. The notion of fibration, that plays an essential rôle in homotopy theory, is tightly related with substitution in dependent type theory. This interplay has led to a new version of type theory called homotopy type theory.

The course is a follow-up of that on category theory taught in the first semester, but can be followed by students who have already some basic background in category theory. We shall introduce the important notions underlying the subject: enriched categories, model categories, as well as different approaches to the definition of higher catégories, notably via simplicial sets. We shall also hint at connected subjects such as operads and ∞-operads, that also have arisen from topology. The lectures will partly follow the flow of exposition found in recent books (Categorical homotopy theory by Emily Riehl, The homotopy theory of (∞, 1)-categories by Julia Bergner, From categories to homotopy theory by Birgit Richter, Higher categories and homotopical algebra by Denis-Charles Cisinski, Simplicial methods for higher categories by Simona Paoli, which all offer opportunities to the interested students for learning more), with an eye on the links with homotopy type theory.

This course aims to present the logical and computational foundations of blockchains (communication protocols, game theory), as well as examples of protocols implemented in particular in crypto-currencies and smart-contracts. We will devote a substantial part of the course to the examination of "decentralized finance", i.e. all the existing chain contracts which postpone and in some cases extend financial practices.

How is logic formal?

The course will be devoted to this question. In particular, we will examine three main reasons for declaring logic "formal": because it uses discursive resources that can be said to be formal (schematic); because it concerns forms (whose status is to be specified: "logical constants" for Russell, "forms derived from something in general" for Husserl, to mention two important examples); and because it aims at an independent validity of any particular content (logic as universal science).

These three main reasons are not necessarily compatible. Moreover, the examination of the question raised will of course imply taking into account the history of logic, and a reflection on the situation of logic between philosophy and mathematics. This will be an opportunity to examine the issue of "absolute generality", that is, the possibility of a theory covering absolutely everything in general.

Aim of the class: knowledge of the philosophical issues of the history of logic in the 20th century.