Rybakov proved that the admissible rules of the intuitionistic propositional calculus are decidable. We give a proof of the same theorem, using the same core idea, but couched in the many notions that have been developed in the mean time. In particular, we illustrate how the argument can be interpreted as using refinements of the notions of exactness and extendibility.

Many intermediate logics, even extremely well-behaved ones such as the intuitionistic propositional calculus, lack the finite model property for admissible rules. We give conditions under which this failure holds. We show that frames which validate all admissible rules necessarily satisfy a certain closure condition, and we prove that this condition, in the finite case, ensures that the frame is of width 2. Finally, we indicate how this result is related to some classical results on finite, free Heyting algebras.

Refutation systems are formal systems for inductively arriving at the non-derivability of formulae. In particular one can use refutation systems to syntactically characterise logics. In this paper we explore the close connection between refutation systems and admissible rules. We develop technical machinery to construct refutation systems, employing techniques from the study of admissible rules. Concretely we provide a refutation system for the intermediate logics of bounded branching, known as the Gabbay-de Jongh logics. To illustrate the technique we also provide a refutation system for Medvedev's logic.

To appear in Notre Dame Journal of Formal Logic
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. Trough 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.

Any intermediate logic with the disjunction property admits the Visser rules if and only if it has the extension property. This equivalence restricts nicely to the extension property up to n. In this paper we demonstrate that the same goes even when omitting the rule ex falso quod libet, that is, working over minimal rather than intuitionistic logic. We lay the groundwork for providing a basis of admissibility for minimal logic, and tie the admissibility of the Mints-Skura rule to the extension property in a stratified manner.

In this paper we study the admissible rules of intermediate logics. We establish some general results on extension of models and sets of formulas. These general results are then employed to provide a basis for the admissible rules of the Gabbay–de Jongh logics and to show that these logics have finitary unification type.