Derivability and Admissibility of Inference Rules in Abstract Hilbert Systems
Clemens Grabmayer · 2003
Abstract. We give an overview of results, presented in the form of a poster at CSL03/KGC, about a general study of the notions of rule derivability and admissibility in Hilbert-style proof systems. The basis of our investigation consists in the concept of “abstract Hilbert system”, a framework for Hilbert-style proof systems in which it is abstracted from the syntax of formulas and the operational content of rules. We Hilbert systems, propose two variant notions of rule derivability, s-derivability and m-derivability, and investigate how these four notions are related. Furthermore, we consider relations that compare abstract Hilbert systems with respect to rule admissibility or with respect to one of the three notions of rule derivability, and study their interrelations. Finally, notions of rule elimination and the notions of rule admissibility and derivability. This paper intends to give a short overview of results presented in the form of a poster with the same title at the 8th Kurt Gödel Colloquium that was jointly