On the Admissible Rules of Intuitionistic Propositional Logic
by
Rosalie Iemhoff
Dept. of Mathematics and Computerscience, University of Amsterdam

The admissible rules of a theory are the rules under which the theory is closed. It is well-known that intuitionistic propositional logic IPC possesses admissible rules which are not derivable. Here we present a basis for the admissible rules of IPC, i.e. a set of rules from which all other admissible rules are derivable. This proves a conjecture of D. de Jongh and A. Visser. Our basis is necessarily infinite, since V. Rybakov proved that there is no finite basis for the admissible rules of IPC. However, the basis is simple in the sense that if we would allow infinite conjunctions it would consist of one scheme. Moreover, together with the disjunction property, this basis characterizes IPC. Namely, for every superintuitionistic logic T it holds that T=IPC iff T has the disjunction property and all the rules in the basis are admissible for T.

http://www.illc.uva.nl/Publications/Lists/www-allseries-1999.html

Date received: March 13, 1999