A(nother) characterization of intuitionistic propositional logic. (English) Zbl 0988.03045

Summary: In a previous paper [the author, J. Symb. Log. 66, 281-294 (2001; Zbl 0986.03013)], we gave a countable basis \({\mathcal V}\) for the admissible rules of IPC. Here, we show that there is no proper superintuitionistic logic with the disjunction property for which all rules in \({\mathcal V}\) are admissible. This shows that, relative to the disjunction property, IPC is maximal with respect to its set of admissible rules. This characterization of IPC is optimal in the sense that no finite subset of \({\mathcal V}\) suffices. In fact, it is shown that for any finite subset \(X\) of \({\mathcal V}\), for one of the proper superintuitionistic logics \(D_n\) constructed by D. de Jongh and D. M. Gabbay [J. Symb. Log. 39, 67-78 (1974; Zbl 0289.02032)], all the rules in \(X\) are admissible. Moreover, the logic \(D_n\) in question is even characterized by \(X\): it is the maximal superintuitionistic logic containing \(D_n\) with the disjunction property for which all rules in \(X\) are admissible. Finally, the characterization of IPC is proved to be effective by showing that it is effectively reducible to an effective characterization of IPC in terms of the Kleene slash by D. de Jongh [in: A. Kino et al. (eds.), Intuitionism and Proof Theory, Proc. Summer Conf. Buffalo/NY 1968, 211-217 (1970; Zbl 0225.02020)].


03B55 Intermediate logics
03B20 Subsystems of classical logic (including intuitionistic logic)
03F50 Metamathematics of constructive systems
Full Text: DOI


[1] D.H.J. de Jongh, A characterization of the intuitionistic propositional calculus, in: A. Kino, J. Myhill, R.E. Vesley (Eds.), Intuitionism and Proof Theory, North-Holland, Amsterdam, 1970. · Zbl 0225.02020
[2] D.H.J. de Jongh, A class of intuitionistic connectives, in: J. Barwise, H.J. Keisler, K. Kunen (Eds.), The Kleene Symposium, North-Holland Publishing Company, Amsterdam, 1980. · Zbl 0479.03015
[3] Gabbay, D.M.; de Jongh, D.H.J., A sequence of decidable finitely axiomatizable intermediate logics with the disjunction property, J. symbolic logic, 39, 67-78, (1974) · Zbl 0289.02032
[4] Iemhoff, R., On the admissible rules of intuitionistic propositional logic, J. symbolic logic, 66, 281-294, (2001) · Zbl 0986.03013
[5] Kleene, S.C., Disjunction and existence under implication in elementary intuitionistic formalisms, J. symbolic logic, 27, 11-18, (1962) · Zbl 0112.24502
[6] Rybakov, V.V., Admissibility of logical inference rules, (1997), Elsevier Amsterdam · Zbl 0872.03002
[7] C.A. Smoryński, Applications of Kripke Models, in: A.S. Troelstra (Ed.), Mathematical Investigations of Intuitionistic Arithmetic and Analysis, Springer, Berlin, 1973.
[8] Troelstra, A.S.; van Dalen, D., Constructivism in mathematics, Vol. I, (1988), North-Holland Amsterdam · Zbl 0653.03040
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.