Requirements Classical Tools in parallel with this course will be a good complement. Program requirements examen Teacher Alexis Saurin and Thomas Colcombet Weekly hours 4 h CM Years Master Logique Mathématique et Fondements de l'Informatique

#### Syllabus

This course will study different aspects of the notion of second order in logic and will study fixed-point logics. In particular, various applications of these logical formalisms to the study of formal languages on words and trees and to the study of programming languages will be discussed.

#### Part 1: Second-order logic and arithmetic, system F

-Syntax of second-order logic, natural second-order deduction, particular theories and fragments (PA2, HA2, MSO, F, ...).

-Second-order models: full models and Henkin models, second-order completeness.

-Proofs and programs: extension of the Curry-Howard correspondence (second-order and polymorphism) and study of the system F (definition, representation of data types, normalization theorems (Girard reducibility candidates, realizability), representative functions in F).

#### Part 2: Logic of the second monadic order

-Definitions, reminders and complements on the theory of automata.

-Decidability on words (Elgott-Büchi-Trakhtenbrot); links with automata and monoids.

-The first-order in the second-order (Schützenberger theorem).

-Decidability on tree-like structures (Courcelle's theorem) and structural bounds on decidability (Seese's theorem).

-The compositional method of Feferman-Vaught and Shelah.

-The theory of infinite words (Büchi, Safra).

-The theory of infinite trees and links with game theory (Rabin, Gurevitch and Harrington).

#### Part 3: Smaller and larger fixed points in logic

-Some results on fixed points.

-Syntaxes and semantics of logics with smaller and larger fixed points (inductive definitions à la Martin-Löf, mu-calculus for classical, intuitionistic and modal logics).

-Deduction systems for fixed-point logics: induction à la Park, Omega rule, circular proofs.

-Relations with automata, with monadic second-order logic.

-Completeness of the mu-calculus and other results.

#### Bibliography

• Rudiments of mu-calculus, A. Arnold and D. Niwinski
• Proofs and Types, JY Girard, P Taylor, Y Lafont
• Proof-theory and Logical complexity, JY Girard -Lambda-calculus and models, JL Krivine
• Proof Theory, Gaisi Takeuti
• Survey of Wolfgang Thomas, Languages, Automata and Logic
• Automata toolbox book https://www.mimuw.edu.pl/~bojan/papers/toolbox.pdf