Master's in Mathematical Logic and Foundations of Computer Science

• 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.

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.

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.

Dans ce cours nous étudierons la théorie des modèles des structures métriques, telles que les espaces de Hilbert et de Banach, les algèbres de probabilité, les systèmes ergodiques ou les algèbres d'opérateurs. Celle-ci est basée sur le formalisme de la logique continue, une généralisation naturelle (à valeurs réelles) de la logique du première ordre classique. Nous étudierons également en détail un fragment distingué de la logique continue, appelé logique affine, et ses connexions toutes récentes avec la théorie de Choquet en analyse fonctionnelle.

On 8 August 1900, at the Second International Congress of Mathematicians in Paris, David Hilbert set out a list of 23 mathematical problems which, in his opinion, should serve as a guide for future research in the new century. The first problem in this list, Cantor's continuum hypothesis, was solved in two stages: by Gödel (1938) who constructed an internal model of the generalized continuum hypothesis, and by Paul Cohen (1963), who invented a model construction for the negation of Cantor's hypothesis. This course will mainly cover the two model constructions of set theory introduced by Gödel and Cohen.

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.

The Curry-Howard correspondence highlights deep links between proofs and programs. Linear logic has profoundly renewed this connection between the formal semantics of programming languages on one hand and proof theory on the other, by bringing attention to the dynamics of programs (how the computation is performed) and on the use of resources. An outcome of this attention to resources are quantitative approaches to calculi, to types and to the semantics. Quantitative systems are able to provide information such as the cost of computation, and are crucial to express paradigms of computation which are intrinsically quantitative, such as probabilistic, differential or quantum computation.

Nous aborderons différents thèmes de complexité. En complexité booléenne, nous parlerons en particulier de complexité de comptage et de complexité de communication. Nous étudierons aussi la complexité algébrique, sur laquelle s'appuient certains efforts récents pour résoudre le problème P vs. NP. En plus d'une présentation générale, nous explorerons des régimes calculatoires restreints, notamment les calculs non-commutatifs, et présenteront certaines bornes inférieures et les techniques de rang qui permettent de les obtenir.

The course is dedicated to the model-checking problem over finite structures, with a particular focus on algorithmic meta-theorems, the main highlight of the course being Courcelle's Theorem.

A number of topics are touched upon through this lens, including some basics in complexity theory, circuit complexity, parameterised complexity, monadic second-order logic, tree languages, logical transductions, structural graph theory, etc.

This is a course on Stone-Priestley duality theory and categorical logic. The main goal is to provide students with the necessary background to be able to start independently reading current research in this field.

We will start from bounded distributive lattices, which are fundamental structures in logic, capturing an extremely basic language that contains as its only primitives "or", "and", "true", and "false". Stone showed that distributive lattices are in a duality with a class of topological spaces with non-trivial specialization order. Priestley re-framed this duality as one between distributive lattices and certain partially ordered topological spaces. Duality theory has since then found applications in a number of areas within logic and the foundations of computer science.

The first part of the course will introduce the mathematical foundations of the theory, also introducing along the way the necessary order theory, topology, and category theory. In the second part of the course, we will discuss applications of the theory to logic, first to intuitionistic propositional and modal logics, and then to higher order logics. This last part will naturally lead to discussing concepts and methods from categorical logic and possibly also topos theory. The precise topics treated in this part will also depend on student interest.

Some basic knowledge of category theory and topology will be helpful, although not strictly required.

The forms of the general