Almost all modal logics are well-known to admit finite cut-free sequent calculi with modal mu-calculus being a notable exception. This calculus extends the basic modal logic K by least and greatest fixed points for all monotone propositional operators. I will present a finitary cut-free axiomatisation for the mu-calculus that features a strengthening of the standard induction rule for greatest fixed point. The system is readily seen to be sound and its completeness is established by utilising a novel calculus of circular proofs which will also be discussed. Furthermore, I will look at how these new calculi relate to Kozen’s original axiomatisation (1983) and the semi-formal system of Jaeger, Kretz and Studer (2008).
Notions of circular or infinitary (non-well-founded) deductive systems naturally arise when one considers fixed point logics, and they have been used for decades in tableaux and sequent calculi for various mu-calculi. However, it is only much more recently that these notions have entered the realm of proofs as computations. In other words, circular proofs have generally been used as an algorithmic trick rather than a proper proof theoretic notion. In this talk, I will describe a general infinitary proof theory. I will attempt to illustrate its beauty and usefulness through various results: cut elimination, translation to finitary proofs, connections with infinite automata theory and completeness for the the linear-time mu-calculus. I will also describe several questions that remain to be explored.
We study a way of expressing all provably total maps of second order arithmetic, which is a possible alternative to system F and to the use of polymorphism. We propose a system we call system N, including data types for well-founded trees, and a recursion schema for data types and all simple types. The recursion schema in system N defines maps on a given data type D and a structure S. The schema simultaneously defines a total map on all possible extensions of the structure S and of the data type D. The schema is used to interpret impredicative definitions in second order arithmetical proofs. In system N we program by extending data structures and maps, in a way which we could be closer to real programming than the use of the entire polymorphism available in system F.
Modal logics have been extensively used for representing and reasoning about complex computational systems. The reasoning tasks for those logics are, however, far from trivial: the local and global satisfiability problems for the basic multimodal propositional logic K are PSPACE-complete and EXPTime-complete, respectively. Given the inherent intractability of the reasoning problems and also the wide range of applications to which those logics can be applied, the development of automatic, efficient tools for theorem proving is highly desirable. In this talk, we will discuss some successful strategies for classical theorem-proving and how they can be adapted for the modal case. We will also report on successful techniques for a resolution-based calculus we have recently developed and implemented for those logics.
In this talk I'll introduce the notion of expansion tree for linear logic. As in Miller's original work, we have a shallow reading of an expansion tree that corresponds to the conclusion of the proof, and a deep reading which is a formula that can be proved by propositional rules. We focus our attention to MLL2, and we also present a deep inference system for that logic. This allows us to give a syntactic proof to a version of Herbrand's theorem.