M2 LMFI: Quantification du second-ordre et points-fixes en logique M2 LMFI: Second-order quantification and fixed points in logic (SOFIX) The 2022-2023 SOFIX course is jointly taught by Thomas Colcombet and Alexis Saurin. See the description of the course on the LMFI website Partie sur la théorie de la preuve du second-ordre et du mu-calcul Part on the proof theory of second-order logic and of the mu-calculus Lecture notes / Notes de cours: 3/01/2023: Lecture 1 by Thomas C. 6/01/2023: Lecture 1 – Proof-program correspondence for Peano's arithmetic (first-order), System T and its normalization theorem, structure of the strong normalization proof by reducibility. lecture notes corresponding to the first lecture (version of the 6/01/22) For Friday 13/01: redo the synthesis of System T recursor from the analysis of Peana Induction axioms seen in class and the proof simplification rules I gave you in class. 10/01/2023: Lecture 2 by Thomas C. 13/01/2023: Lecture 2 – Proving strong normalization for System T. lecture notes corresponding to the second lecture (version of the 17/01/22) For Friday 20/01: do the exercizes in the notes for lecture 2. 17/01/2023: Lecture 3 – Introduction to second-order logic, second-order arithmetic, System F and its normalization properties. (planned) lecture notes corresponding to the third lecture, part on second-order logic For Friday 20/01: derive the remaining PA1 axioms for equality in PA2. 20/01/2023: Lecture 4 – Reducibility candidates and weak normalisation of System F. lecture notes corresponding to the fourth lecture, weak normalization of System F. 24/01/2023: Lecture 3 by Thomas C. 27/01/2023: Lecture 4 by Thomas C. 31/01/2023: Cancelled. 3/02/2023: Lecture 5 – Realizability in System F. lecture notes corresponding to the fifth lecture, realizability for System F **superseded by notes on lecture 6!**. 7/02/2023: Lecture 5 by Thomas C. 10/02/2023: Lecture 6 by Thomas C. 14/02/2023: Lecture 7 by Thomas C. 17/02/2023: Lecture by Thomas C is cancelled 21/02/2023: Lecture 6 – Applications of realizability. lecture notes corresponding to the sixth lecture, SN of F and other application of realizability. For Friday 24/02: do the exercise on the characterization of type Nat. 24/02/2023: Lecture 7 – Expressiveness of System F. 28/02/2023: no lecture: where were you? 3/03/2023: Lecture 8 by Thomas C. 7/03/2023: Cancelled due to strike 8/03/2023: Lectures 8 et 9 – Representation theorem of System F. 10/03/2023: Mid-term exam 14/03/2023: Lecture 9 by Thomas C. 17/03/2023: Lecture 10 by Thomas C. 21/03/2023: ??? 24/03/2023: ??? 28/03/2023: ??? 31/03/2023: ??? Homework / DM: For friday 13/01: redo the synthesis of System T recursor from the analysis of Peano Induction axioms seen in class and the proof simplification rules I gave you in class. For friday 20/01: do the exercizes in the notes for lecture 2. More to come! Bibliographic references / Références bibliographiques: Domains and Lambda-calculi, R. Amadio & P-L. Curien Rudiments of mu-calculus, A. Arnold & D. Niwinski Proofs and Types, J-Y. Girard, P. Taylor & Y. Lafont Proof-theory and Logical Complexity, J-Y. Girard Practical Foundations for Programming Languages, R. Harper Lambda-calculus and Models, J-L. Krivine Lectures on the Curry-Howard Isomorphism, M. H. Sørensen & P. Urzyczyn Proof Theory, G. Takeuti Some old lecture notes, to be updated: Basic proof theory and lambda-calculus (corresponding to first semester course): Part of the first semester course on proof-theory dedicated to natural deduction and the lambda-calculus Some notes on second-order logic and System F Gödel's system T (normalization and expressive power) (version of the 7/01/22) Introduction to second-order logic and arithmetics (version of the 7/01/22) Introduction to System F and its normalization properties (version of the 13/01/22)