Cut-elimination for non-wellfounded proofs
Lukas Zenger, University of Bern
In standard proof theory a proof is a finite tree whose nodes are labelled by sequents and which is generated by a finite set of rules. One such rule is the cut rule, which is a sequent calculus analogue of the well-known modus ponens rule. As the cut rule introduces new formulas into a proof, it makes proofs non-analytic. Therefore, much effort is devoted to show that the cut rule can be eliminated from a given calculus without changing the set of derivable sequents. Such a cut-elimination theorem is established by showing how instances of the cut rule in a given proof can be pushed upwards until the premises of the instances are axioms. One then shows that in this case the instances of cut can be eliminated from the proof. However, this standard strategy does not work when one considers so-called non-wellfounded proofs, which are proofs in which some branches are allowed to be infinitely long. Clearly, in such a setting it is not enough to simply push instances of cut upwards, as a leaf might never be reached. In this talk I will present ongoing research on cut-elimination for non-wellfounded proofs for a fragment of the modal mu-calculus. I will discuss the basic idea how to construct a cut-free proof from a given non-wellfounded proof and present some of the current problems of my method.