Research project Circular reasoning: exploring the power of non-wellfounded proofs
The standard approach in proof theory is to view a proof as a finite, wellfounded structure, in which the conclusion is justified stepwise by a chain of inference steps grounded in an axiom. I explore how non-wellfounded proof systems allow never-ending chains of inference steps, or cycles, where the conclusion to be derived is assumed as a premise.
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.
Project description
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.
Project members
Project managers
Sebastian Enqvist
Universitetslektor
