Circular reasoning: exploring the power of non-wellfounded proofs

This project is about non-wellfounded and circular proof systems, particularly in the context of (modal) fixpoint logics.

The standard approach in proof theory is to view a proof as a finite, wellfounded structure, in which the conclusion is justified step by step by a chain of inference steps that is eventually grounded in an axiom.

By contrast, non-wellfounded proof systems allow never-ending chains of inference steps, or cycles where the conclusion to be derived is assumed as a premise.

Rather than being grounded in axioms, such inferences are considered valid or not depending on some global constraints on the structure of a proof.

Non-wellfounded proof systems are natural and useful tools for dealing with logics for reasoning about induction and co-induction (fixpoint logics), witnessed by an extensive and growing literature.

Recently, circular proofs have played a key role in some substantial advancements in the proof theory of modal fixpoint logics.

They were used to prove a cut-free completeness result for the modal mu-calculus, and later to prove completeness of Parikh´s dynamic logic of games.

In this project, I will follow up on this development with the aim of developing complete proof systems for modal fixpoint logics, especially expressive extensions of the modal mu-calculus.

I will also study translations between different proof systems, and clarify some philosophical and conceptual questions regarding the status of circular reasoning in logic and mathematics.