Room P3.10, Mathematics Building

João Rasga, Instituto Superior Técnico

Sufficient conditions for cut elimination in first order based calculi

Sufficient conditions for a sequent calculus to enjoy cut elimination are established for a wide class of first order based logics. The conditions result from the application of traditional cut elimination proof techniques to an arbitrary calculus composed by rules that must satisfy a number of reasonable conditions. Based on the cut elimination theorem, the subformula property and the consistency of these calculi are established.