Model Theory Makes Formulas Large

Gaifman’s locality theorem states that every first-order sentence is equivalent to a local sentence. We show that there is no elementary bound on the length of the local sentence in terms of the original. The classical Ło´s-Tarski theorem states that every first-order sentence preserved under extensions is equivalent to an existential sentence. We show that there is no elementary bound on the length of the existential sentence in terms of the original. Recently, variants of the Ło´s-Tarski theorem have been proved for certain classes of finite structures, among them the class of finite acyclic structures and more generally classes of structures of bounded tree width. Our lower bound also applies to these variants. We further prove that a version of the Feferman-Vaught theorem based on a restriction by formula length necessarily entails a non-elementary blow-up in formula size. All these results are based on a similar technique of encoding large numbers by trees of small heigh...

• Type: Conference
• Year: 2007
• Where: ICALP
• Authors: Anuj Dawar, Martin Grohe, Stephan Kreutzer, Nicole Schweikardt
• Keywords: Existential Sentence, ICALP 2007, Local Sentence, Theoretical Computer Science, first-order Sentence