Model theory is the study of the interaction between formulas in some logical formalism and their models, that is, structures that satisfy the formulas. There are two directions in this interaction, namely, from syntax to semantics and from semantics to syntax. The rst direction aims to identify structural properties possessed by all models of formulas having common syntactic features. For example, it is easy to show that every universal rst-order sentence is preserved under substructures. The second direction aims to characterize formulas in terms of their structural properties. For example, the well known Los-Tarski Theorem asserts that if a rst-order sentence is preserved under substructures, then it is logically equivalent to a universal rst-order sentence. In general, establishing results in the second direction is a much harder task than establishing results in the rst. In other words, obtaining model-theoretic characterizations of formulas or of classes of formulas is a far greater challenge than identifying structural properties possessed by all models of formulas with common syntactic features. Makowsky and Vardi [9] were the rst to obtain model-theoretic characterizations of classes of database dependencies expressed in suitable fragments of rst-order logic. Furthermore, they classi ed the work on model-theoretic characterizations into two distinct approaches, which they called the preservation and the axiomatizability approach: Preservation Approach. One considers two logical formalisms L and L0, where L0 is typically a proper fragment of L, and the goal is to obtain modeltheoretic characterizations of the following form: a set of L-formulas is equivalent to a set 0 of L0-formulas if and only if the models of satisfy certain structural properties. For example, the Los-Tarski Theorem is a prime example in the preservation approach. Axiomatizability Approach. One considers a logical formalism L, and the goal is to obtain model-theoretic characterizations of the following form: a class C of structures is axiomatizable by a (possibly in nite) set of Lformulas if and only if the structures in C satisfy certain structural properties. Makowsky and Vardi [9] further distinguished the special case of nite axiomatizability, where the goal is to obtain model-theoretic characterizations of when a class of structures is axiomatizable by a nite set of L-formulas. They
then obtained model-theoretic characterizations of axiomatizability and nite axiomatizability of classes of database dependencies.
Database dependencies were originally used to formalize integrity constraints
in databases with much of the early work in this area focusing on the implication
problem between database dependencies (see [
Several model-theoretic characterizations following the preservation approach
have been established for tgds [
Summary of Results. Motivated by the preceding state of a airs, we embark here on a systematic investigation of model-theoretic characterizations of classes of tgds in the nite axiomatizability approach. This investigation is carried out in the context of ontologies. From a syntactic point of view, an ontology is speci ed by a set of formulas in some formalism. From a semantic point of view, an ontology can be identi ed with the set of all structures ( nite or in nite) that satisfy the formulas specifying the ontology. Hence, as a semantic object, an ontology is an isomorphism-closed class of ( nite or in nite) structures over some xed relational schema. Our goal is to answer the following question: what are necessary and su cient conditions for an ontology (an isomorphism-closed class of structures) to be speci ed by a set of tgds? The main outcome of this investigation is to characterize the ontologies that are nitely axiomatizable by a nite set of arbitrary tgds or by a nite set of tgds that belong to one of the main subclasses of tgds, namely, full, frontier-guarded, guarded, and linear tgds.
Our model-theoretic characterizations make use of structural properties encountered in earlier model-theoretic characterizations, such as the ontology being closed under direct products, and containing critical structures of every nite cardinality, where a structure is critical if each of its relations contains all possible tuples from the domain of the structure. The main innovation, however, is the introduction and use of the notion of (n; m)-locality, where, intuitively, n represents the number of universal quanti ers in the tgds and m represents the number of existential quanti ers in the tgds. Our rst main result asserts that an ontology O is axiomatizable by a nite set of tgds if and only if O is closed under direct products, contains critical structures of every nite cardinality, and is (n; m)-local for some non-negative integers n and m. The notion of (n; m)locality turns out to be delicate, yet exible. Indeed, this notion can be tailored to other classes of tgds, so that it gives rise to the re ned notions of frontierguarded (n; m)-locality, guarded (n; m)-locality, and linear (n; m)-locality. Using these re ned notions, we obtain model-theoretic characterizations of ontologies that are axiomatizable by a nite set of, respectively, frontier-guarded, guarded, and linear tgds.
Acknowledgments. Part of Marco Console's work was done while he was a research associate at the University of Edinburgh. Part of Andreas Pieris' work was done while he was visiting the University of California, Santa Cruz. Marco Console has been partially supported by MIUR under the PRIN 2017 project \HOPE" (prot. 2017MMJJRE), and by the EU under the H2020-EU.2.1.1 project TAILOR, grant id. 952215. Phokion Kolaitis has been partially supported by NSF Award No. 1814152. Andreas Pieris was supported by the EPSRC grant EP/S003800/1 \EQUID".