Kripke sheaf completeness of some superintuitionistic predicate logics with a weakened constant domains principle (Q454383)

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.