License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2013.61
URN: urn:nbn:de:0030-drops-41907
Go to the corresponding LIPIcs Volume Portal

Berkholz, Christoph ; Krebs, Andreas ; Verbitsky, Oleg

Bounds for the quantifier depth in finite-variable logics: Alternation hierarchy

10.pdf (0.6 MB)


Given two structures G and H distinguishable in FO^k (first-order logic with k variables), let A^k(G,H) denote the minimum alternation depth of a FO^k formula distinguishing G from H. Let A^k(n) be the maximum value of A^k(G,H) over n-element structures. We prove the strictness of the quantifier alternation hierarchy of FO^2 in a strong quantitative form, namely A^2(n) >= n/8-2, which is tight up to a constant factor. For each k >= 2, it holds that A^k(n) > log_(k+1) n-2 even over colored trees, which is also tight up to a constant factor if k >= 3. For k >= 3 the last lower bound holds also over uncolored trees, while the alternation hierarchy of FO^2 collapses even over all uncolored graphs.
We also show examples of colored graphs G and H on n vertices that can be distinguished in FO^2 much more succinctly if the alternation number is increased just by one: while in Sigma_i it is possible to distinguish G from H with bounded quantifier depth, in Pi_i this requires quantifier depth Omega(n2). The quadratic lower bound is best possible here because, if G and H can be distinguished in FO^k with i quantifier alternations, this can be done with quantifier depth n^(2k-2).

BibTeX - Entry

  author =	{Christoph Berkholz and Andreas Krebs and Oleg Verbitsky},
  title =	{{Bounds for the quantifier depth in finite-variable logics: Alternation hierarchy}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{61--80},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Simona Ronchi Della Rocca},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-41907},
  doi =		{10.4230/LIPIcs.CSL.2013.61},
  annote =	{Keywords: Alternation hierarchy, finite-variable logic}

Keywords: Alternation hierarchy, finite-variable logic
Collection: Computer Science Logic 2013 (CSL 2013)
Issue Date: 2013
Date of publication: 02.09.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI