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

TL;DR

This paper investigates how different propositional connectives influence the relationship between intuitionistic predicate logic and the logic of constant domains by extending Kripke semantics to first-order logic.

Contribution

It extends generalized Kripke semantics to first-order logic and provides a necessary and sufficient condition for when intuitionistic predicate logic matches the logic of constant domains.

Findings

Identifies connectives that cause divergence between the two logics

Provides a criterion for when the logics coincide

Enhances understanding of semantics in intuitionistic logic

Abstract

It is known that intuitionistic Kripke semantics can be generalized so that it can treat arbitrary propositional connectives characterized by truth functions. We extend this 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 terms of validity of sequents. Our main result gives 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.