On Semantic Generalizations of the Bernays-Sch\"onfinkel-Ramsey Class with Finite or Co-finite Spectra

TL;DR

This paper introduces a semantic family of first-order logic classes with finite or co-finite spectra, generalizing the Bernays-Schönfinkel-Ramsey class and exploring their properties, lattice structure, and relationships to known classes.

Contribution

It defines the EBS_\Sigma(\sigma) classes, analyzes their properties, lattice structure, and semantic equivalences, providing a semantic generalization of BSR and alternative proofs of classical results.

Findings

EBS_\Sigma classes are spectrally indistinguishable.

EBS_\Sigma(\Sigma) is semantically equivalent to BSR.

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