Cyclic proofs, a primer

Advanced course at the 37th European Summer School in Logic, Language and Information, 2026.
Lectured by Prof. Anupam Das.

Cyclic and non-wellfounded proofs have emerged in the last 30 years as a powerful mechanism to reason about systems with (co)inductive predicates or data. They are an alternative to usual well-founded proofs with (co)induction principles, that are seemingly more powerful at the level of expressivity, and more intuitive at the level of proof search, often avoiding elusive invariants.

This course will introduce students to the foundations of cyclic proof systems, based in the theories of extremal fixed points, combinatorial games and ω-automaton theory. Our working case study will be the modal μ-calculus, a prototypical setting that exemplifies well the peculiarities of non-wellfounded proofs. This case study notwithtanding, the course aims to give students the robust tools needed to apply these techniques to new logics and theories.

Outline of the course

The lectures will provisionally be structured as follows (to be updated during the week):

  • Lecture 1 (Monday). Fixed points of monotone operators. Motivating examples, monotone operators on complete lattices, Knaster-Tarski fixed point theorem, approximants, induction and coinduction.
    [board 1][board 2][board 3][board 4][board 5][board 6][exercises][answers] (updated 03/08/26).
    Accessibility: This lecture has no dependencies and should be accessible to all ESSLLI participants with some mathematical background.
  • Lecture 2 (Tuesday). Modal logic with fixed points. Syntax and semantics of the μ-calculus, examples of (nested) fixed points, non-wellfounded proof system, examples of cyclic proofs.
    [board 1][board 2][board 3][board 4][board 5][board 6][board 7][exercises]
    Accessibility: This lecture builds on Lecture 1, but should still be accessible to most ESSLLI participants.
  • Lecture 3 (Wednesday, updated 05/08/26). The μ-calculus and evaluation games. More on the μ-calculus, functors and induction, evaluation games and their adequacy, soundness of non-wellfounded proofs (time permitting).
    [board 1][board 2][board 3][board 4][board 5][board 6][board 7][exercises]
    Accessibility: This lecture builds on Lectures 1 and 2.
  • Lecture 4 (Thursday, updated 06/08/2026). Finite memory determinacy and completeness for the μ-calculus. Parity games, positional determinacy, proof search games, completeness of cyclic proofs.
    [board 1][board 2][board 3][board 4][board 5][board 6][exercises]
    Accessibility: The first half of this lecture may be followed largely independently of the previous 3 lectures. The second part, on proof search games and completeness, builds on the previous three lectures.
  • Lecture 5 (Friday, updated 10/08/2026). Completeness and further directions. Completeness of non-wellfounded proofs, effectivity via ω-automata, further examples, historical context.
    [board 1][board 2][board 3][board 4][board 5][board 6]
    Accessibility: The first part of this lecture builds on all previous lectures, the final part is a non-technical and survey-style, and should be accessible to all ESSLLI participants.

Prerequisites and scope

As an advanced course, there are two recommended prerequisites:

  • Some background in proof theory or tableaux systems.
  • Some background in basic modal logic syntax and semantics.

Some parts of the course, in particular the first lecture, should be accessible to all participants, regardless of background. More fine-grained dependencies can be found in the outline above.

Other than this, any familiarity with fixed points, (co)induction, and infinite automaton theory will be helpful, but not necessary. Let us point out that the focus of this course will not be proof theory, per se, focussing rather on proof systems and their metalogical properties. We shall also largely gloss over the automaton-theoretic aspects behind cyclic proofs, in the interest of time (e.g. McNaughton’s theorem and the Büchi-Landweber theorem).

Bibliographic notes

There is unfortunately a lack of introductory reading for non-experts in cyclic proofs; indeed the point of this course is to try expose the subject to a wider audience. Nonetheless, it should be mentioned that the genesis of the subject is arguably in the following paper:

This course can be seen as a modern presentation of the results therein. It should also be mentioned that Yde Venema has draft lecture notes on the μ-calculus. The most recent version I can find is here (please let me know if you have a more recent version).

There are many many papers on cyclic and non-wellfounded proofs, depending on the perspective at hand (algebra, linear logic, modal logic, type theory, predicate logic,…). There are too many to share here but please do just ask me if you are interested in any particular direction and I can try point you to some useful references. I may add further references here during the week.

➤