Logic Journal of IGPL

Logic Journal of IGPL Advance Access originally published online on October 16, 2007
Logic Journal of IGPL 2007 15(5-6):653-687; doi:10.1093/jigpal/jzm051

This Article Abstract Full Text (PDF) Alert me when this article is cited Alert me if a correction is posted Services Email this article to a friend Similar articles in this journal Alert me to new issues of the journal Add to My Personal Archive Download to citation manager Request Permissions Google Scholar Articles by Krynicki, M. Articles by Torres, J. M. T. Search for Related Content Social Bookmarking          What's this?

© The Author, 2007. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Games on Trees and Syntactical Complexity of Formulas

Micha Krynicki

Faculty of Mathematics and Natural Sciences, Cardinal Stefan Wyszyski University, Dewajtis 5, 01-815 Warsaw, Poland. E-mail: m.krynicki{at}uksw.edu.pl

Jose Maria Turull Torres

Information Science Research Centre, Dept. of Information Systems, Massey University, Private Box 756, Wellington, New Zealand. E-mail: J.M.Turull{at}massey.ac.nz

Ehrenfeucht-Fraïssé games have been introduced as a means of characterizing the relation of elementary equivalence between structures, or relational database instances in first order logic (FO), or equivalently Relational Calculus. Inthe usual Ehrenfeucht-Fraïssé games the rules are determined by a linear ordering of a fixed lenght or, equivalently, by a special kind of tree – a chain of a fixed length –, where each point of that ordering or node of that tree corresponds to a quantification operation. Here we consider Ehrenfeucht-Fraïssé games whose rules are determined by arbitrary trees such that their nodes correspond either to quantification operations ("q–nodes") or to connective operations ("c–nodes"). By playing games on trees, we can refine the class of sentences which are considered in a given game, since a tree represents a particular class of sentences. We define and study several variations of tree games, for first and second order logic (SO). We give a sufficient condition for FO and SO equivalence restricted to formulae with up to n connectives, and hence also a sufficient condition for the non expressibility of a given query in those logics with formulae whose number of logical connectives is less than a given integer. We also give a sufficient condition to prove simultaneous lower bounds in both the number of connectives and in the quantifier types needed to express a given property in FO. If we consider only quantifier types, we get a characterization of the relation of preservation of sentences in the fragment of FO with the given set of quantifier types. We also study tree games for _n and _n formulae. To illustrate the use of our games we use them to prove lower bounds in the connective size for several FO queries, like size of a database, size of a clique in a graph, size of a unary relation, transitive property in a graph, and degree of a node in a graph. Regarding SO, we prove lower bounds for quantifier rank for the parity query.

Finally, we give a precise characterization of the logic whose elementary equivalence is characterized by a given tree game, as well as several equivalent characterizations of the existence of a winning strategy for Duplicator in the classical Ehrenfeucht-Fraïssé game.

Key Words: Ehrenfeucht-Fraisse games • games on trees • definability • syntactical complexity.

Received for publication 15 September 2006.

References

1. Abiteboul S, Hull R, Vianu V. "Foundations of Databases". (1995) Addison-Wesley.

2. Barwise J. "The syntax and semantics of infinitary languages". In: LNM 72 (1968) Springer Verlag.

3. Barwise J. "On Moschovakis Closure Ordinals". Journal of Symbolic Logic (1977) 42:292–296.[CrossRef][ISI]

4. Chang C, Keisler H. "Model Theory". (1992) 3rd ed. Elsevier North Holland.

5. Dickman MA. "Large Infinitary Languages". (1975) Nort–Holland Publishing Company.

6. Ebbinghaus H, Flum J. "Finite Model Theory". (1999) 2nd. ed. Springer Verlag.

7. Ehrenfeucht A. "An Application of Games to the Completeness Problem for Formalized Theories". Fundamenta Mathematicae (1961) 49:129–141.

8. Fraïssé R. "Sur Quelques Classifications des Systèmes de Relations (english summary). (1954) 1. Série A: Université d'Alger, Publications Scientifiques. 35–182.

9. Hintikka J, Sandu G. "Game–theoretical semantics". In: "Handbook of Logic and Language"—van Benthem J, ter Meulen A, eds. (1997) Elsevier Publ. Comp. 361–410.

10. Immerman N. "Upper and Lower Bounds for First Order Expressibility". Journal of Computer and System Sciences (1982) 25(1):76–98.[CrossRef][ISI]

11. Immerman N, Kozen D. "Definability with a bounded number of bound variables". Information and Computation (1989) 83:121–139.[CrossRef][ISI]

12. Krawczyk A, Krynicki M. "Ehrenfeucht games for generalized quantifiers". LNM 537 (1976) 145–152.

13. Krynicki M, Szczerba LW. "On Simplicity of formulae". In: Studia Logica 49 (1990) 401–419.

14. Krynicki M, Turull Torres JM. "Lower Bounds in the number of Connectives in First Order Logic". In: Technical Report 7/2005 (2005) Massey University.

15. Krynicki M, Turull Torres JM. "Games on Trees and Syntactical Complexity of Formulas". In: Technical Report 3/2006 (2006) Massey University.

16. Poizat B. "Deux ou trois choses que je sais de L_n". Journal of Symbolic Logic (1982) 47:641–658.[CrossRef][ISI]

17. Tenney R. "Second–order Ehrenfeucht games and the decidability of the second order theory of an equivalence relation". Journal of the Australian Mathematical Society (1975) 20:323–331.

18. Väänänen J. "Games and Trees in Infinitary Logic: A Survey". "Quantifiers: Logics, Models and Computation" Volume One: Surveys—Krynicki M, Mostowski M, Szczerba LW, eds. (1995) Kluwer Academic Publishers.

19. Weese M. "Generalized Ehrenfeucht games". Fundamenta Mathematicae (1980) 109:103–112.

CiteULike    Connotea    Del.icio.us    What's this?

This Article Abstract Full Text (PDF) Alert me when this article is cited Alert me if a correction is posted Services Email this article to a friend Similar articles in this journal Alert me to new issues of the journal Add to My Personal Archive Download to citation manager Request Permissions Google Scholar Articles by Krynicki, M. Articles by Torres, J. M. T. Search for Related Content Social Bookmarking          What's this?