Kripke sheaf completeness of some superintuitionistic predicate logics with a weakened constant domains principle. (English) Zbl 1258.03031

The paper analyzes the completeness of the combinations of \(\mathbf{QH}\), the intuitionistic predicate logic, with the axioms \(D^* \equiv \forall x (P(x) \vee Q) \rightarrow Q \vee \forall x \exists y (P(y) \&\neg\neg[x = y])\), the weak constant domain principle, \(K \equiv \neg\neg \forall x (P(x) \vee \neg P(x))\), the Kuroda principle, and \(J \equiv \neg Q \vee \neg\neg Q\), the weak excluded middle principle.
The completeness of the considered systems is developed in the class of Kripke frames with equality, which is equivalent to Kripke sheaves. It is worth noticing how all the considered systems are incomplete in the standard Kripke semantics, where equality is the diagonal relation in each possible world.
Extending the techniques developed in his previous works, the author establishes appropriate completeness results for \((\mathbf{QH} + D^*)\), \((\mathbf{QH} + D^* \&K)\), and \((\mathbf{QH} + D^* \&K \&J)\). Also, the paper proves that the system \((\mathbf{QH} + D^* \&J)\) is incomplete with respect to the considered semantics.
Some discussions about how these intermediate systems can be considered as the Kripke completions of other intermediate logics, e.g., \((\mathbf{QH} + E \&K\&J)\), where \(E\) is a variant of the Markov principle, complete the article.


03B55 Intermediate logics
Full Text: DOI


[1] Corsi G., Ghilardi S.: ’Directed frames’. Archive for Math. Logic 29, 53–67 (1989) · Zbl 0689.03009
[2] Dragalin, A. G., Mathematical intuitionism. Introduction to proof theory, Translations of Mathematical Monographs 67, AMS, 1988. · Zbl 0634.03054
[3] Gabbay D.M.: ’Applications of trees to intermediate logics’. Journal of Symbolic Logic 37, 135–138 (1972) · Zbl 0243.02019
[4] 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. · Zbl 1211.03002
[5] Ghilardi S.: ’Presheaf semantics and independence results for some non-classical first-order logics’. Archive for Math. Logic 29, 125–136 (1989) · Zbl 0691.03013
[6] Ono H.: ’Incompleteness of semantics for intermediate predicate logics. I: Kripke’s semantics’. Proc. Jap. Acad. 49, 711–713 (1973) · Zbl 0299.02026
[7] Ono H.: ’Model extension theorem and Craig’s interpolation theorem for intermediate predicate logics’. Reports on Math. Logic 15, 41–58 (1983) · Zbl 0519.03016
[8] 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). · Zbl 0788.03022
[9] 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) · Zbl 0772.03008
[10] Skvortsov D.: ’On the predicate logic of finite Kripke frames’. Studia Logica 54, 79–88 (1995) · Zbl 0839.03011
[11] Skvortsov D.: ’On intermediate predicate logics of some finite Kripke frames, I. Levelwise uniform trees’. Studia Logica 77, 295–323 (2004) · Zbl 1073.03013
[12] Skvortsov D.: ’On the predicate logic of linear Kripke frames and some its extensions’. Studia Logica 81, 261–282 (2005) · Zbl 1092.03013
[13] Skvortsov D., ’On the difference between constant domains principle and its weakened versions in the Kripke sheaf semantics’, In preparation.
[14] Skvortsov D., ’The Kripke sheaf completion of the superintuitionistic predicate logic with weak constant domains principle’, In preparation. · Zbl 1258.03031
[15] Skvortsov D., ’On some weakened versions of constant domains principle in the Kripke sheaf semantics’, In preparation.
[16] 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.
[17] Suzuki N.-Y.: ’Some results on the Kripke sheaf semantics for super-intuitionistic predicate logics’. Studia Logica 52, 73–94 (1993) · Zbl 0772.03009
[18] 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) · Zbl 0661.03015
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.