Archive 2022
RequirementsFollowing the course Proofs-Programming: Classical Tools in parallel with this course will be a good complement.
Program requirementsCC+examen
TeacherAlexis Saurin and Thomas Colcombet
Weekly hours 48 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