Abstract
The completeness w.r.t. Kripke frames with equality (or, equivalently, w.r.t. Kripke sheaves, [8] or [4, Sect. 3.6]) is established for three superintuitionistic predicate logics: (Q-H + D*), (Q-H + D*&K), (Q-H + D*&K&J). Here Q-H is intuitionistic predicate logic, J is the principle of the weak excluded middle, K is Kuroda’s axiom, and D* (cf. [12]) is a weakened version of the well-known constant domains principle D. Namely, the formula D states that any individual has ancestors in earlier worlds, and D* states that any individual has \({\neg\neg}\) -ancestors (i.e., ancestors up to \({\neg\neg}\) -equality) in earlier worlds. In particular, the logic (Q-H + D*&K&J) is the Kripke sheaf completion of (Q-H + E&K&J), where E is a version of Markov’s principle (cf. [12]). On the other hand, we show that the logic (Q-H + D*&J) is incomplete w.r.t. Kripke sheaves.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Corsi G., Ghilardi S.: ‘Directed frames’. Archive for Math. Logic 29, 53–67 (1989)
Dragalin, A. G., Mathematical intuitionism. Introduction to proof theory, Translations of Mathematical Monographs 67, AMS, 1988.
Gabbay D.M.: ‘Applications of trees to intermediate logics’. Journal of Symbolic Logic 37, 135–138 (1972)
Gabbay, D., V. Shehtman, and D. Skvortsov, Quantification in nonclassical logic, Vol. 1, Sections 2.6, 2.14, 3.6, 5.1, 5.2, 5.6, Studies in Logic and the Foundations of Mathematics 153, Elsevier, 2009.
Ghilardi S.: ‘Presheaf semantics and independence results for some non-classical first-order logics’. Archive for Math. Logic 29, 125–136 (1989)
Ono H.: ‘Incompleteness of semantics for intermediate predicate logics. I: Kripke’s semantics’. Proc. Jap. Acad. 49, 711–713 (1973)
Ono H.: ‘Model extension theorem and Craig’s interpolation theorem for intermediate predicate logics’. Reports on Math. Logic 15, 41–58 (1983)
Shehtman, V., and D. Skvortsov, ‘Semantics of non-classical first order predicate logics’, in P. Petkov (ed.), Mathematical Logic, Plenum Press, N.Y., 1990, pp. 105–116. (Proc. of Summer school and conference in math. logic Heyting’88).
Shimura T.: ‘Kripke completeness of some intermediate predicate logics with the axiom of constant domain and a variant of canonical formulas’. Studia Logica 52, 23–40 (1993)
Skvortsov D.: ‘On the predicate logic of finite Kripke frames’. Studia Logica 54, 79–88 (1995)
Skvortsov D.: ‘On intermediate predicate logics of some finite Kripke frames, I. Levelwise uniform trees’. Studia Logica 77, 295–323 (2004)
Skvortsov D.: ‘On the predicate logic of linear Kripke frames and some its extensions’. Studia Logica 81, 261–282 (2005)
Skvortsov D., ‘On the difference between constant domains principle and its weakened versions in the Kripke sheaf semantics’, In preparation.
Skvortsov D., ‘The Kripke sheaf completion of the superintuitionistic predicate logic with weak constant domains principle’, In preparation.
Skvortsov D., ‘On some weakened versions of constant domains principle in the Kripke sheaf semantics’, In preparation.
Smoryński, C., ‘Applications of Kripke models’, in A. S. Troelstra (ed.), Metamathematical investigation of intuitionistic arithmetic and analysis, Lecture Notes Math. 344:324–391, Springer, 1973.
Suzuki N.-Y.: ‘Some results on the Kripke sheaf semantics for super-intuitionistic predicate logics’. Studia Logica 52, 73–94 (1993)
Yokota S.: ‘Axiomatization of the first-order intermediate logics of bounded Kripkean heights. I’, Zeitschr. für math. Logik und Grundl. der Math. 35, 415–421 (1989)
Author information
Authors and Affiliations
Corresponding author
Additional information
In memoriam Leo Esakia
Rights and permissions
About this article
Cite this article
Skvortsov, D. Kripke Sheaf Completeness of some Superintuitionistic Predicate Logics with a Weakened Constant Domains Principle. Stud Logica 100, 361–383 (2012). https://doi.org/10.1007/s11225-012-9382-2
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11225-012-9382-2