Computability in Europe 2006
Logical Approaches to Computational Barriers

Invited Plenary Talk:
Proof systems for admissibility

Speaker: Rosalie Iemhoff
Author(s): Rosalie Iemhoff and George Metcalfe


Proof systems for admissibility.

Admissibility is a generalization of derivability that for classical logics coincide with it. This, however, is in general not the case for nonclassical logics. A rule is called admissible for a logic if the extension of the logic by this rule does not lead to new theorems. For many well-known modal and intermediate logics characterizations of their admissible rules in the form of a semantics or a set of rules have been known for some time, but proof systems for admissibility were still missing.

In the talk we will present proof systems for admissibility (in Gentzen style) that have cut elimination and a form of the subformula property. The systems all share a core part, to which, for a particular logic, only some rules specific for that logic have to be added to make it into a complete proof system for the admissible rules of that logic. These systems cover many nonclassical logics, for example extensions of the modal logic K4, intuitionistic logic, and Jankov logic. One of the useful properties of these proof systems is that from the underivability of a rule in a system a substitution that falsifies the admissibility of the rule in the logic corresponding to the system can be read off.

This is joint work with George Metcalfe.

websites: Arnold Beckmann 2008-06-06