Admissible and derivable rules in intuitionistic logic
Paul Rozière · Mathematical Structures in Computer Science · 1993
This paper gives some sufficient conditions for admissible rules to be derivable in intuitionistic propositional calculus. For example, if the premises are Harrop formulas, the rule is admissible only if it is derivable. In deriving the results, a particular class of substitutes is introduced, which are also useful when dealing with other questions of admissibility.