RequirementsClassical Tools in parallel with this course will be a good complement.
Program requirementsexamen
TeacherAlexis Saurin and Thomas Colcombet
Weekly hours 4 h CM
Years

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.

Contents

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