A (Semantic) Characterization of Cut-elimination

Cut-elimination is one of the most important techniques in proof theory. Roughly speaking, eliminating cuts from a proof generates a new proof without lemmas, which essentially consists of the syntactic material of the proven theorem. Since its introduction in 1934, sequent calculus has been one of the preferred deductive frameworks to formalize and reason about logics. However, this framework is not capable of handling all interesting and useful logics. To this end, a large range of variants and extensions of Gentzen sequent calculi have been introduced in the last few decades. Among them, hypersequent calculus has been shown to be a rather elegant and simple framework for "logic engineering" that applies to a wide range of non-classical logics . The aim of the proposed project is a semantic characterization of cut-elimination in sequent and hypersequent calculi, i.e. the definition of syntactic and semantic criteria that when satisfied by such calculi guarantee a certain kind of cut-elimination, and when not satisfied, provide counterexamples. The central idea is to answer the following questions: Which are the natural properties that rules have to satisfy in order to preserve cut-elimination? Is there a uniform method to prove (or disprove) cut-elimination for a wide class of sequent or hypersequent calculi? The main advantages of such a method would be: 1. it becomes easier to prove cut-elimination theorems for novel (sequent type) logic calculi and to find analytic calculi for new logics 2. the construction of the cut-elimination methods and the checking of the formal criteria can be automated - provided the method is effective.

Cut-elimination is one of the most important techniques in proof theory. Roughly speaking, eliminating cuts from a proof generates a new proof without lemmas, which essentially consists of the syntactic material of the proven theorem. Since its introduction in 1934, sequent calculus has been one of the preferred deductive frameworks to formalize and reason about logics. However, this framework is not capable of handling all interesting and useful logics. To this end, a large range of variants and extensions of Gentzen sequent calculi have been introduced in the last few decades. Among them, hypersequent calculus has been shown to be a rather elegant and simple framework for ``logic engineering`` that applies to a wide range of non-classical logics . The aim of the proposed project is a semantic characterization of cut-elimination in sequent and hypersequent calculi, i.e. the definition of syntactic and semantic criteria that when satisfied by such calculi guarantee a certain kind of cut-elimination, and when not satisfied, provide counterexamples. The central idea is to answer the following questions: Which are the natural properties that rules have to satisfy in order to preserve cut-elimination? Is there a uniform method to prove (or disprove) cut-elimination for a wide class of sequent or hypersequent calculi? The main advantages of such a method would be: 1. it becomes easier to prove cut-elimination theorems for novel (sequent type) logic calculi and to find analytic calculi for new logics 2. the construction of the cut-elimination methods and the checking of the formal criteria can be automated - provided the method is effective.