Computer Science Logic and 8th Kurt Gödel Colloquium R. Iemhoff: Towards a proof system for admissibility

Welcome and News Host Institutions Calls and Deadlines Program Social Program Registration Location and Venue Accommodation Committees Contact Colocated Events Authors' instructions

Print this page An interesting meta-mathematical property of intuitionistic propositional logic IPC is the existence of non-derivable admissible rules for this logic. Some years ago it was shown that a certain class of rules, so-called Visser's rules, form a basis for the admissible rules of IPC. Intuitively this means that all the admissible rules of IPC can be obtained from Visser's rules via derivability in IPC. Here we strengthen this result by presenting a system ADM that consists of Visser's rules and a finite number of simple rewriting rules, such that for every formula A the system ADM derives a formula B such that the the admissibly derivable consequences of A are the (normal) consequences of B. Note that this result implies that V is a basis for the admissible rules of IPC. However, it is stronger in the sense that it provides more information about the admissibility relation. © 2002-2003 Kurt Gödel Society, Norbert Preining. 2003-06-04