On Semantic Generalizations of the Bernays-Schönfinkel-Ramsey Class with Finite or Co-finite Spectra

Abstract

Motivated by model-theoretic properties of the BSR class, we present a family of semantic classes of FO formulae with finite or co-finite spectra over a relational vocabulary Σ. A class in this family is denoted EBS_Σ(σ), where σis a subset of Σ. Formulae in EBS_Σ(σ) are preserved under substructures modulo a bounded core and modulo re-interpretation of predicates outside σ. We study properties of the family EBS_Σ= {EBS_Σ(σ) | σ\subseteq Σ}, e.g. classes in EBS_Σare spectrally indistinguishable, EBS_Σ(Σ) is semantically equivalent to BSR over Σ, and EBS_Σ(\emptyset) is the set of all FO formulae over Σwith finite or co-finite spectra. Furthermore, (EBS_Σ, \subseteq) forms a lattice isomorphic to the powerset lattice (\wp(Σ), \subseteq). This gives a natural semantic generalization of BSR as ascending chains in (EBS_Σ, \subseteq). Many well-known FO classes are semantically subsumed by EBS_Σ(Σ) or EBS_Σ(\emptyset). Our study provides alternative proofs of interesting results like the Loś-Tarski Theorem and the semantic subsumption of the Löwenheim class with equality by BSR. We also present a syntactic sub-class of EBS_Σ(σ) called EDP_Σ(σ) and give an expression for the size of the bounded cores of models of EDP_Σ(σ) formulae. We show that the EDP_Σ(σ) classes also form a lattice structure. Finally, we study some closure properties and applications of the classes presented.

arXiv comment26 pages, no figures, submitted to LICS 2010 (decision pending); just added a reference to a related work in this version