Title :
Homomorphism closed vs. existential positive
Author :
Feder, Tomás ; Vardi, Moshe Y.
Author_Institution :
Stanford Univ., CA, USA
Abstract :
Preservations theorems, which establish connection between syntactic and semantic properties of formulas, are a major topic of investigation in model theory. In the context of finite-model theory, most, but not all, preservation theorems are known to fail. It is not known, however, whether the Los-Tarski-Lyndon theorem, which asserts that a first-order sentence is preserved under homomorphisms if it is equivalent to an existential positive sentence, holds with respect to finite structures. Resolving this is an important open question in finite-model theory. In this paper we study the relationship between closure under homomorphism and positive syntax for several nonfirst-order existential logics that are of interest in computer science. We prove that the Los-Tarski-Lyndon theorem holds for these logics. The logics we consider are variable-confined existential infinitary logic, Datalog, and various fragments of second-order logic.
Keywords :
finite automata; formal logic; logic programming; theorem proving; Los-Tarski-Lyndon theorem; computer science; datalog; existential positive; finite structure; finite-model theory; homomorphism; infinitary logic; positive syntax; preservations theorem; second-order logic; semantic property; syntactic property; Computer science; Context modeling; Databases; Logic functions; Terminology;
Conference_Titel :
Logic in Computer Science, 2003. Proceedings. 18th Annual IEEE Symposium on
Print_ISBN :
0-7695-1884-2
DOI :
10.1109/LICS.2003.1210071