×

zbMATH — the first resource for mathematics

Intermediate logics and Visser’s rules. (English) Zbl 1102.03032
A set \(R\) of admissible rules forms a basis of admissible rules for a logic \(L\) if all the admissible rules of \(L\) can be derived from \(R\). It was proved by the author [J. Symb. Log. 66, 281–294 (2001; Zbl 0986.03013)] that the so-called Visser’s rules form a basis of admissible rules for the intuitionistic propositional calculus IPC. This paper discusses bases of admissible rules for other intermediate logics.
The paper shows that if all Visser’s rules are admissible for an intermediate logic \(L\), then Visser’s rules form a basis for \(L\). This implies that if all Visser’s rules are derivable in \(L\), then all the admissible rules of \(L\) are derivable. As a result, the author obtains that the Dummett logic LC of linear Kripke frames does not have non-derivable admissible rules.
The paper also gives a criterion for admissibility of Visser’s rules. Namely, it is shown that Visser’s rules are admissible (and therefore, by the result mentioned above, form a basis) for an intermediate logic \(L\) iff \(L\) has the offspring property (which is a special kind of an extension property).
As a corollary, the author derives that Visser’s rules are admissible for the intermediate logic KC of all directed Kripke frames, and that there exist logics with the disjunction property for which not all Visser’s rules are admissible.

MSC:
03B55 Intermediate logics
03B35 Mechanization of proofs and logical operations
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Baaz, M., A. Ciabattoni, and C. G. Fermüller, ”Hypersequent calculi for Gödel logics—A survey”, Journal of Logic and Computation , vol. 13 (2003), pp. 835–61. · Zbl 1051.03046 · doi:10.1093/logcom/13.6.835
[2] Blackburn, P., M. de Rijke, and Y. Venema, Modal Logic , vol. 53 of Cambridge Tracts in Theoretical Computer Science , Cambridge University Press, Cambridge, 2001. · Zbl 0988.03006
[3] Chagrov, A., and M. Zakharyaschev, Modal Logic , vol. 35 of Oxford Logic Guides , The Clarendon Press, New York, 1997. · Zbl 0871.03007
[4] Dummett, M., ”A propositional calculus with denumerable matrix”, The Journal of Symbolic Logic , vol. 24 (1959), pp. 97–106. JSTOR: · Zbl 0089.24307 · doi:10.2307/2964753 · links.jstor.org
[5] Gabbay, D. M., and D. H. J. De Jongh, ”A sequence of decidable finitely axiomatizable intermediate logics with the disjunction property”, The Journal of Symbolic Logic , vol. 39 (1974), pp. 67–78. JSTOR: · Zbl 0289.02032 · doi:10.2307/2272344 · links.jstor.org
[6] Ghilardi, S., ”Unification in intuitionistic logic”, The Journal of Symbolic Logic , vol. 64 (1999), pp. 859–80. JSTOR: · Zbl 0930.03009 · doi:10.2307/2586506 · links.jstor.org
[7] Ghilardi, S., ”A resolution/tableaux algorithm for projective approximations in IPC”, Logic Journal of the IGPL , vol. 10 (2002), pp. 229–43. · Zbl 1005.03504 · doi:10.1093/jigpal/10.3.229
[8] Gödel, K., ”Über Unabhängigkeitsbeweise im Aussagenkalkül”, Ergebnisse eines mathematischen Kolloquiums , vol. 4 (1933), pp. 9–10. · JFM 59.0865.02
[9] Iemhoff, R., ”On the admissible rules of intuitionistic propositional logic”, The Journal of Symbolic Logic , vol. 66 (2001), pp. 281–94. JSTOR: · Zbl 0986.03013 · doi:10.2307/2694922 · links.jstor.org
[10] Iemhoff, R., ”A(nother) characterization of intuitionistic propositional logic”, Annals of Pure and Applied Logic , vol. 113 (2002), pp. 161–73. First St. Petersburg Conference on Days of Logic and Computability (1999). · Zbl 0988.03045 · doi:10.1016/S0168-0072(01)00056-2
[11] Iemhoff, R., ”Towards a proof system for admissibility”, pp. 255–70 in Computer Science Logic , vol. 2803 of Lecture Notes in Computer Science , Springer, Berlin, 2003. · Zbl 1116.03304
[12] Kreisel, G., and H. Putnam, ”Eine Unableitbarkeitsbeweismethode für den intuitionistischen Aussagenkalkul”, Archiv für mathematische Logic und Grundlagenforschung , vol. 3 (1957), pp. 74–78. · Zbl 0079.00702 · doi:10.1007/BF01988049 · eudml:137735
[13] Roziere, P., Regles Admissibles en Calcul Propositionnel Intuitionniste , Ph.D. thesis, Université Paris VII, 1992.
[14] Rybakov, V. V., Admissibility of Logical Inference Rules , vol. 136 of Studies in Logic and the Foundations of Mathematics , North-Holland Publishing Co., Amsterdam, 1997. · Zbl 0872.03002
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.