What Kinds of Connectives Cause the Difference Between Intuitionistic Predicate Logic and the Logic of Constant Domains?

Abstract

It is known that intuitionistic Kripke semantics can be generalized so that it can treat arbitrary propositional connectives characterized by truth functions. Our previous work studied how the choice of propositional connectives changes the relation between classical and intuitionistic propositional logics, and showed that the set of valid sequents in intuitionistic propositional logic coincides with the set of valid sequents in classical propositional logic if and only if the connectives we choose are all monotonic. In this paper, we extend the generalized Kripke semantics to first-order logic and study how the choice of connectives changes the relation between intuitionistic predicate logic and the logic of constant domains. In the case of the usual connectives ¬, ∧, ∨, and →, it is well-known that the presence of disjunction causes the difference between these two logics. Generalizing this result to general propositional connectives, we give a simple necessary and sufficient condition for the set of valid sequents in intuitionistic predicate logic to coincide with the set of valid sequents in the logic of constant domains.