First-order modal logic: Kripke semantics and its challenges

This talk is an introduction to first-order modal logic with a focus on first-order extensions of propositional Kripke semantics. Incorporating quantifiers and modal operators introduces challenges in maintaining the axioms and rules of classical first-order and propositional modal logic while undergoing minimal alterations. Even a straightforward extension of propositional modal logic K to the first-order level validates certain versions of the Barcan formulas, leading to formulations with problematic readings. I will introduce first-order Kripke semantics with constant domains, demonstrating the validity of Barcan formulas in such semantics. Subsequently, I will explore how employing first-order Kripke semantics with varying domains can invalidate the Barcan formulas, albeit at the expense of sacrificing some classical first-order rules.