First order S4 and its measure-theoretic semantics

The first order modal logic FOS4 is a combination of the axioms and rules of inference of propositional S4 and classical first order logic with identity. We give a topological and measure-theoretic semantics for FOS4 with expanding domains. The latter extends the measure-theoretic semantics for propositional S4 introduced by Scott and studied in [3] and [6], and [8]. The main result of the paper is that FOS4 is complete for the measure-theoretic semantics with countable expanding domains. More formally, FOS  4 is complete for the Lebesgue measure algebra, MM, or algebra of Borel subsets of the real line modulo sets of measure zero, with countable expanding domains. A corollary to the main result is that first order intuitionistic logic FOH   is complete for the frame of open elements in MM with countable expanding domains. We also show that FOS4 is not complete for the real line or the infinite binary tree with limits with countable expanding domains.