The Admissible Rules of BD2 and GSc

Abstract

The Visser rules form a basis of admissibility for the intuitionistic propositional calculus. We show how one can characterise the existence of covers in certain models, by means of formulae. Through this characterisation, we provide a new proof of the admissibility of a weak form of the Visser rules. Finally, we use this observation, coupled with a description of a generalisation of the disjunction property, to provide a basis of admissibility for the intermediate logics BD2 and GSc.