Model Theory of Monadic Predicate Logic with the Infinity Quantifier

Abstract

This paper establishes model-theoretic properties of \(\mathrm{FOE}^{\infty}\), a variation of monadic first-order logic that features the generalised quantifier \(\exists^\infty\) (`there are infinitely many'). We provide syntactically defined fragments of \(\mathrm{FOE}^{\infty}\) characterising four different semantic properties of \(\mathrm{FOE}^{\infty}\)-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 \(\varphi^{p}\) belonging to the corresponding syntactic fragment, with the property that \(\varphi\) is equivalent to \(\varphi^{p}\) 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 (\(\mathrm{FOE}\)) and without (\(\mathrm{FO}\)) equality, and then move to \(\mathrm{FOE}^{\infty}\) by including the generalised quantifier \(\exists^\infty\) into the picture. As a corollary of our developments, we obtain that the four semantic properties above are decidable for \(\mathrm{FOE}^{\infty}\)-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.