semantic characterization of cut-elimination

01.03.2006 - 30.11.2009
Research funding project
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 calculi have been shown shown to be a rather elegant and simple framework for ``logic engineering'' that applies to a wide range of nonclassical logics arising in several areas of mathematics, philosophy and computer science. 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, provides 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 automatized - provided the method is effective

People

Project leader

Project personnel

Institute

Grant funds

  • FWF - Österr. Wissenschaftsfonds (National) Austrian Science Fund (FWF)

Research focus

  • Computational Intelligence: 100%

Keywords

GermanEnglish
hypersequent calculihypersequent calculi
cut eliminationcut elimination
proof theoryproof theory
non classical logicsnon classical logics

Publications