Model Theory of Monadic Predicate Logic with the Infinity Quantifier

This paper establishes model-theoretic properties of FOE∞, a variation of monadic first-order logic that features the generalised quantifier exists^∞ (`there are infinitely many'). We provide syntactically defined fragments of FOE∞ characterising four different semantic properties of FOE∞-sentences: (1) being monotone and (2) (Scott) continuous in a given set of monadic predicates; (3) having truth preserved under taking submodels or (4) invariant under taking quotients. In each case, we produce an effectively defined map that translates an arbitrary sentence varphi to a sentence varphip belonging to the corresponding syntactic fragment, with the property that varphi is equivalent to varphip precisely when it has the associated semantic property. Our methodology is first to provide these results in the simpler setting of monadic first-order logic with (FOE) and without (FO) equality, and then move to FOE∞ by including the generalised quantifier exists^∞ into the picture. As a corollary of our developments, we obtain that the four semantic properties above are decidable for FOE∞-sentences. Moreover, our results are directly relevant to the characterisation of automata and expressiveness modulo bisimilirity for variants of monadic second-order logic. This application is developed in a companion paper.