A(nother) characterization of intuitionistic propositional logic Original Research Article

In Iemhoff (J. Symbolic Logic, to appear) we gave a countable basis View the MathML source for the admissible rules of View the MathML source. Here, we show that there is no proper superintuitionistic logic with the disjunction property for which all rules in View the MathML source are admissible. This shows that, relative to the disjunction property, View the MathML source is maximal with respect to its set of admissible rules. This characterization of View the MathML source is optimal in the sense that no finite subset of View the MathML source suffices. In fact, it is shown that for any finite subset X of View the MathML source, for one of the proper superintuitionistic logics Dn constructed by De Jongh and Gabbay (J. Symbolic Logic 39 (1974)), all the rules in X are admissible. Moreover, the logic Dn in question is even characterized by X: it is the maximal superintuitionistic logic containing Dn with the disjunction property for which all rules in X are admissible. Finally, the characterization of View the MathML source is proved to be effective by showing that it is effectively reducible to an effective characterization of View the MathML source in terms of the Kleene slash by De Jongh (Kino et al. eds., Intuitionism and Proof Theory, North-Holland, Amsterdam, 1970).