(Semantic) Characterization of Cut-Elimination




General Information
Abstract
People
Publications
Related Projects

General Information

The project, funded by the Austrian Science Fund ( FWF ), has started in March 2006 and lasted until November 2009.

Project leader: Dr. Agata Ciabattoni.

Project Abstract

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:

People

The following researchers were employed in the project:

Project Publications

Journals (Peer-reviewed) Conferences

Related Projects