===== 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 [[https://master.math.univ-paris-diderot.fr/modules/m2lmfi-second-ordre/|description of the course]] on the LMFI website /* === Presentation of research papers === [[https://www.irif.fr/users/saurin/teaching/lmfi/sofix-2022/paper-presentation|Page listing papers for the presentation]] */ === 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.** * [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix-2023/cours-01.pdf|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. /*(additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-1.pdf|whiteboard]])*/ * 10/01/2023: Lecture 2 by Thomas C. * 13/01/2023: **Lecture 2 -- Proving strong normalization for System T.** * [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix-2023/cours-02.pdf|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. /*[[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix2.pdf|Introduction to second-order logic and arithmetics]] (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-2.pdf|whiteboard]])*/ * 17/01/2023: **Lecture 3 -- Introduction to second-order logic, second-order arithmetic, System F and its normalization properties.** (planned) * [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix-2023/cours-03.pdf|lecture notes corresponding to the third lecture, part on second-order logic]] /* * [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix-2023/cours-03.pdf|lecture notes corresponding to the third lecture, part on Church-style system F]]*/ * For Friday 20/01: derive the remaining PA1 axioms for equality in PA2. /* [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix3.pdf|Introduction to System F and its normalization properties]] (version of the 13/01/22) (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-3.pdf|whiteboard]])*/ * 20/01/2023: **Lecture 4 -- Reducibility candidates and weak normalisation of System F.** * [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix-2023/cours-04.pdf|lecture notes corresponding to the fourth lecture, weak normalization of System F.]] /* (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-4.pdf|whiteboard]], until slide 11)*/ * 24/01/2023: Lecture 3 by Thomas C. * 27/01/2023: Lecture 4 by Thomas C. * 31/01/2023: **Cancelled.** /* (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-5.pdf|whiteboard]]) */ * 3/02/2023: **Lecture 5 -- Realizability in System F.** * [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix-2023/cours-05.pdf|lecture notes corresponding to the fifth lecture, realizability for System F **superseded by notes on lecture 6!**.]] /* (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-6.pdf|whiteboard]])*/ * 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.** * [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix-2023/cours-06.pdf|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.** /* Full models and Henkin models of second-order logic, completeness of second-order logic wrt. Henkin's models.** (planned) (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-7.pdf|whiteboard]])*/ /* (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-8.pdf|whiteboard]])*/ * 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.** /* **Lecture 9.** */ * 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: ??? /* * **Lecture 8 -- Representation theorem of system F** (planned). * **Lecture 9 -- Representation of free structures in system F.** (planned) /* (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-9.pdf|whiteboard]])*/ * **Lecture 10 -- Proof theory of the mu-calculus.** (planned) /* (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-10.pdf|whiteboard]])*/ * **Lecture 11 -- Proof systems for the (modal) mu-calculus: 2- Infinitary Proof systems for the mu-calculus** (planned) /* (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-11.pdf|whiteboard]])*/ * **Lecture 12 -- Proof systems for the (modal) mu-calculus: 3- Infinitary proofs with the Omega-rule, relations with other proof systems.** (planned) /* (additional material: [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/whiteboard-sofix-12.pdf|whiteboard]])*/ */ == 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): * [[https://www.irif.fr/users/saurin/teaching/lmfi/cf-thdem-2021|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 * [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix1.pdf|Gödel's system T (normalization and expressive power)]] (version of the 7/01/22) * [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix2.pdf|Introduction to second-order logic and arithmetics]] (version of the 7/01/22) * [[https://www.irif.fr/_media/users/saurin/teaching/lmfi/sofix3.pdf|Introduction to System F and its normalization properties]] (version of the 13/01/22)