The admissible rules of \(\mathsf{BD}_2\) and \(\mathsf{GSc}\). (English) Zbl 1455.03034

Goudsmit, Jeroen P.

Notre Dame J. Formal Logic 59, No. 3, 325-353 (2018).

Summary: The Visser rules form a basis of admissibility for the intuitionistic propositional calculus. We show how one can characterize the existence of covers in certain models by means of formulae. Through this characterization, 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 generalization of the disjunction property, to provide a basis of admissibility for the intermediate logics \({{\mathsf{BD}_{2}}}\) and \({\mathsf{GSc}}\).

MSC:

03B55	Intermediate logics
03B20	Subsystems of classical logic (including intuitionistic logic)

Keywords:

admissible rules; intermediate logics; intuitionistic logic; universal model

References:

[1]	Anderson, J. G., “An application of Kripke’s completeness theorem for intuitionism to superconstructive propositional calculi,” Zeitschrift für mathematische Logik und Grundlagen der Mathematik, vol. 15 (1969), pp. 259–88. · Zbl 0216.28802 · doi:10.1002/malq.19690151603
[2]	Avellone, A., M. Ferrari, and P. Miglioli, “Duplication-free tableau calculi and related cut-free sequent calculi for the interpolable propositional intermediate logics,” Logic Journal of the IGPL, vol. 7 (1999), pp. 447–80. · Zbl 0938.03042 · doi:10.1093/jigpal/7.4.447
[3]	Balbes, R., and A. Horn, “Injective and projective Heyting algebras,” Transactions of the American Mathematical Society, vol. 148 (1970), pp. 549–59. · Zbl 0199.32203 · doi:10.1090/S0002-9947-1970-0256952-1
[4]	Bellissima, F., “Finitely generated free Heyting algebras,” Journal of Symbolic Logic, vol. 51 (1986), pp. 152–65. · Zbl 0616.03021 · doi:10.2307/2273952
[5]	Bezhanishvili, G., and N. Bezhanishvili, “Profinite Heyting algebras,” Order, vol. 25 (2008), pp. 211–27. · Zbl 1155.06007 · doi:10.1007/s11083-008-9089-1
[6]	Bezhanishvili, G., and S. Ghilardi, “An algebraic approach to subframe logics: Intuitionistic case,” Annals of Pure and Applied Logic, vol. 147 (2007), pp. 84–100. · Zbl 1123.03055 · doi:10.1016/j.apal.2007.04.001
[7]	Chagrov, A., and M. Zakharyaschev, Modal Logic, vol. 35 of Oxford Logic Guides, Oxford University Press, New York, 1997. · Zbl 0871.03007
[8]	Cintula, P., and G. Metcalfe, “Admissible rules in the implication-negation fragment of intuitionistic logic,” Annals of Pure and Applied Logic, vol. 162 (2010), pp. 162–71. · Zbl 1225.03011 · doi:10.1016/j.apal.2010.09.001
[9]	Citkin, A., “Structurally complete superintuitionistic logics,” Doklady Akademii Nauk SSSR, vol. 241 (1978), pp. 40–3; English translation in Soviet Mathematics Doklady, vol. 19 (1978), pp. 816–19. · Zbl 0412.03009
[10]	Citkin, A., “A note on admissible rules and the disjunction property in intermediate logics,” Archive for Mathematical Logic, vol. 51 (2012), pp. 1–14. · Zbl 1248.03047 · doi:10.1007/s00153-011-0250-y
[11]	Citkin, A., “Not every splitting Heyting or interior algebra is finitely presentable,” Studia Logica, vol. 100 (2012), pp. 115–35. · Zbl 1258.06003 · doi:10.1007/s11225-012-9391-1
[12]	Darnière, L., and M. Junker, “On Bellissima’s construction of the finitely generated free Heyting algebras, and beyond,” Archive for Mathematical Logic, vol. 49 (2010), pp. 743–71. · Zbl 1215.06004
[13]	de Jongh, D. H. J., and A. S. Troelstra, “On the connection of partially ordered sets with some pseudo-Boolean algebras,” Indagationes Mathematicae, vol. 28 (1966), pp. 317–29. · Zbl 0137.02203
[14]	de Jongh, D. H. J., and F. Yang, “Jankov’s theorems for intermediate logics in the setting of universal models,” pp. 53–76 in Logic, Language, and Computation, edited by N. Bezhanishvili, S. Löbner, K. Schwabe, and L. Spada, vol. 6618 of Lecture Notes in Computer Science, Springer, Berlin, 2011. · Zbl 1341.03036
[15]	Dummett, M., “A propositional calculus with denumerable matrix,” Journal of Symbolic Logic, vol. 24 (1959), pp. 97–106. · Zbl 0089.24307 · doi:10.2307/2964753
[16]	Dzik, W., and A. Wroński, “Structural completeness of Gödel’s and Dummett’s propositional calculi,” Studia Logica, vol. 32 (1973), pp. 69–75. · Zbl 0345.02036
[17]	Elageili, R., and J. K. Truss, “Finitely generated free Heyting algebras: The well-founded initial segment,” Journal of Symbolic Logic, vol. 77 (2012), pp. 1291–307. · Zbl 1272.03163 · doi:10.2178/jsl.7704140
[18]	Gabbay, D. M., and D. H. J. de Jongh, “A sequence of decidable finitely axiomatizable intermediate logics with the disjunction property,” Journal of Symbolic Logic, vol. 39 (1974), pp. 67–78. · Zbl 0289.02032 · doi:10.2307/2272344
[19]	Ghilardi, S., “Unification through projectivity,” Journal of Logic and Computation, vol. 7 (1997), pp. 733–52. · Zbl 0894.08004 · doi:10.1093/logcom/7.6.733
[20]	Ghilardi, S., “Unification in intuitionistic logic,” Journal of Symbolic Logic, vol. 64 (1999), pp. 859–80. · Zbl 0930.03009 · doi:10.2307/2586506
[21]	Ghilardi, S., “Unification, finite duality and projectivity in varieties of Heyting algebras,” Annals of Pure and Applied Logic, vol. 127 (2004), pp. 99–115. · Zbl 1058.03020 · doi:10.1016/j.apal.2003.11.010
[22]	Goudsmit, J. P., and R. Iemhoff, “On unification and admissible rules in Gabbay–de Jongh logics,” Annals of Pure and Applied Logic, vol. 165 (2014), pp. 652–72. · Zbl 1316.03016 · doi:10.1016/j.apal.2013.09.003
[23]	Grätzer, G., Lattice Theory: Foundation, Springer Basel, 2011. · Zbl 1233.06001
[24]	Harrop, R., “Concerning formulas of the types \(A→ B∨ C\), \(A→(∃ x)B(x)\) in intuitionistic formal systems,” Journal of Symbolic Logic, vol. 25 (1960), pp. 27–32. · Zbl 0098.24201
[25]	Hosoi, T., “On intermediate logics, I,” Journal of the Faculty of Science, University of Tokyo. Section 1, vol. 14 (1967), pp. 293–312. · Zbl 0188.31602
[26]	Iemhoff, R., “On the admissible rules of intuitionistic propositional logic,” Journal of Symbolic Logic, vol. 66 (2001), pp. 281–94. · Zbl 0986.03013 · doi:10.2307/2694922
[27]	Iemhoff, R., “A(nother) characterization of intuitionistic propositional logic,” Annals of Pure and Applied Logic, vol. 113 (2002), pp. 161–73. · Zbl 0988.03045 · doi:10.1016/S0168-0072(01)00056-2
[28]	Iemhoff, R., “Intermediate logics and Visser’s rules,” Notre Dame Journal of Formal Logic, vol. 46 (2005), pp. 65–81. · Zbl 1102.03032 · doi:10.1305/ndjfl/1107220674
[29]	Iemhoff, R., “On the rules of intermediate logics,” Archive for Mathematical Logic, vol. 45 (2006), pp. 581–99. · Zbl 1096.03025 · doi:10.1007/s00153-006-0320-8
[30]	Iemhoff, R., and G. Metcalfe, “Proof theory for admissible rules,” Annals of Pure and Applied Logic, vol. 159 (2009), pp. 171–86. · Zbl 1174.03024 · doi:10.1016/j.apal.2008.10.011
[31]	Jankov, V. A., “Some superconstructive propositional calculi,” Doklady Akademii Nauk SSSR, vol. 151 (1963), pp. 796–98; English translation in Soviet Mathematics Doklady, vol. 4 (1963), pp. 1103–05. · Zbl 0143.25102
[32]	Jeřábek, E., “Admissible rules of modal logics,” Journal of Logic and Computation, vol. 15 (2005), pp. 411–31. · Zbl 1077.03011
[33]	Jeřábek, E., “Independent bases of admissible rules,” Logic Journal of the IGPL, vol. 16 (2008), pp. 249–67. · Zbl 1146.03008
[34]	Jeřábek, E., “Bases of admissible rules of Łukasiewicz logic,” Journal of Logic and Computation, vol. 20 (2010), pp. 1149–63. · Zbl 1216.03043
[35]	Kracht, M., “Book review: V. V. Rybakov. Admissibility of Logical Inference Rules,” Notre Dame Journal of Formal Logic, vol. 40 (1999), pp. 578–87.
[36]	Maksimova, L. L., “Pretabular superintuitionistic logics,” Algebra i Logika, vol. 11 (1972), pp. 558–70, 615; English translation in Algebra and Logic, vol. 11 (1972), pp. 308–14. · Zbl 0275.02027
[37]	Maksimova, L. L., “Interpolation properties of superintuitionistic logics,” Studia Logica, vol. 38 (1979), pp. 419–28. · Zbl 0435.03021 · doi:10.1007/BF00370479
[38]	Maksimova, L. L., “On maximal intermediate logics with the disjunction property,” Studia Logica, vol. 45 (1986), pp. 69–75. · Zbl 0635.03019 · doi:10.1007/BF01881550
[39]	McKay, C. G., “Some completeness results for intermediate propositional logics,” Notre Dame Journal of Formal Logic, vol. 8 (1967), pp. 191–94. · Zbl 0183.00904
[40]	Mints, G. E., “Derivability of admissible rules,” Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta Imeni V. A. Steklova, vol. 32, pp. 85–9; English translation in Journal of Soviet Mathematics, vol. 6 (1976), pp. 417–21. · Zbl 0358.02031
[41]	Odintsov, S., and V. V. Rybakov, “Unification and admissible rules for paraconsistent minimal Johanssons’ logic \({\mathbf{J}}\) and positive intuitionistic logic \({\mathbf{IPC} }+\),” Annals of Pure and Applied Logic, vol. 164 (2013), pp. 771–84. · Zbl 1323.03029 · doi:10.1016/j.apal.2013.01.001
[42]	Prucnal, T., “On two problems of Harvey Friedman,” Studia Logica, vol. 38 (1979), pp. 247–62. · Zbl 0436.03018 · doi:10.1007/BF00405383
[43]	Renardel de Lavalette, G. R., A. Hendriks, and D. H. J. de Jongh, “Intuitionistic implication without disjunction,” Journal of Logic and Computation, vol. 22 (2012), pp. 375–404. · Zbl 1258.03014 · doi:10.1093/logcom/exq058
[44]	Rose, G. F., “Review: V. A. Jankov and S. Walker. Some Superconstructive Propositional Calculi,” Journal of Symbolic Logic, vol. 35 (1970), pp. 138–39.
[45]	Rybakov, V. V., “Rules of inference with parameters for intuitionistic logic,” Journal of Symbolic Logic, vol. 57 (1992), pp. 912–23. · Zbl 0788.03007 · doi:10.2307/2275439
[46]	Rybakov, V. V., Admissibility of Logical Inference Rules, vol. 136 of Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1997. · Zbl 0872.03002
[47]	Scott, D., “Rules and derived rules,” pp. 147–61 in Logical Theory and Semantic Analysis: Essays Dedicated to Stig Kanger on His Fiftieth Birthday, edited by S. Stenlund, vol. 63 of Synthese Library, Springer, Boston, 1974. · Zbl 0296.02012
[48]	Shoesmith, D. J., and T. J. Smiley, Multiple-Conclusion Logic, Cambridge University Press, Cambridge, 1978. · Zbl 0381.03001
[49]	Skura, T. F., “A complete syntactical characterization of the intuitionistic logic,” Reports on Mathematical Logic, vol. 23 (1989), pp. 75–80. · Zbl 0809.03007
[50]	Skura, T. F., “Refutation calculi for certain intermediate propositional logics,” Notre Dame Journal of Formal Logic, vol. 33 (1992), pp. 552–60. · Zbl 0789.03021 · doi:10.1305/ndjfl/1093634486
[51]	Smoryński, C. A., “Applications of Kripke models,” pp. 324–91 in Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, edited by A. S. Troelstra, vol. 344 of Lecture Notes in Mathematics, Springer, Berlin, 1973. · Zbl 0275.02025
[52]	Terese, Term Rewriting Systems, vol. 55 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge, 2003. · Zbl 1030.68053
[53]	Troelstra, A. S., “On intermediate propositional logics,” Indagationes Mathematicae, vol. 27 (1965), pp. 141–52. · Zbl 0143.01102
[54]	Troelstra, A. S., and D. van Dalen, “Logic,” pp. 35–111 in Constructivism in Mathematics, I, vol. 121 of Studies in Logic and the Foundations of Mathematics, Elsevier, Amsterdam, 1988. · Zbl 0653.03040
[55]	Wójcicki, R., Theory of Logical Calculi: Basic Theory of Consequence Operations, vol. 199 of Synthese Library, Kluwer, Dordrecht, 1988. · Zbl 0682.03001
[56]	Zakharyaschev, M., “Canonical formulas for K4, I: Basic results,” Journal of Symbolic Logic, vol. 57 (1992), pp. 1377–402. · Zbl 0774.03005 · doi:10.2307/2275372
[57]	Zakharyaschev, M., “Canonical formulas for K4, II: Cofinal subframe logics,” Journal of Symbolic Logic, vol. 61 (1996), pp. 421–49. · Zbl 0884.03014 · doi:10.2307/2275669