The Visser rules form a basis of admissibility for the intuitionistic propositional calculus. We show how one can characterize the existence of covers in certain models by means of formulae. Through this characterization, 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 generalization of the disjunction property, to provide a basis of admissibility for the intermediate logics 𝖡𝖣2 and GSc.

Publication
Goudsmit () The Admissible Rules of BD2 and GSc. Notre Dame Journal of Formal Logic, 59(3):325-353 doi: 10.1215/00294527-3838972