
An interesting metamathematical property of intuitionistic propositional logic IPC is the existence of nonderivable admissible rules for this logic. Some years ago it was shown that a certain class of rules, socalled 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.
© 20022003 Kurt Gödel Society, Norbert Preining. 
20030604
 