Research project Circular reasoning: exploring the power of non-wellfounded proofs
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.
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.