Structure Theorem and Strict Alternation Hierarchy for FO^2 on Words

DOI10.2168/LMCS-5(3:4)2009zbMATH Open1168.03019arXiv0907.0616MaRDI QIDQ3395099FDOQ3395099

Authors: Philipp Weis, Neil Immerman 

Publication date: 20 August 2009

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: It is well-known that every first-order property on words is expressible using at most three variables. The subclass of properties expressible with only two variables is also quite interesting and well-studied. We prove precise structure theorems that characterize the exact expressive power of first-order logic with two variables on words. Our results apply to both the case with and without a successor relation. For both languages, our structure theorems show exactly what is expressible using a given quantifier depth, n, and using m blocks of alternating quantifiers, for any m leq n. Using these characterizations, we prove, among other results, that there is a strict hierarchy of alternating quantifiers for both languages. The question whether there was such a hierarchy had been completely open. As another consequence of our structural results, we show that satisfiability for first-order logic with two variables without successor, which is NEXP-complete in general, becomes NP-complete once we only consider alphabets of a bounded size.

Full work available at URL: https://arxiv.org/abs/0907.0616

Recommendations

• Structure Theorem and Strict Alternation Hierarchy for FO2 on Words
• Algebraic characterization of the alternation hierarchy in \(\mathrm{FO}^2[<]\) on finite words
• Quantifier alternation in two-variable first-order logic with successor is decidable
• On FO 2 Quantifier Alternation over Words
• The \(\mathrm{FO}^2\) alternation hierarchy is decidable

zbMATH Keywords

finite model theorydescriptive complexityalternation hierarchyEhrenfeucht-Fraïssé games

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Model theory of finite structures (03C13) Automata and formal grammars in connection with logical questions (03D05) Temporal logic (03B44) Basic properties of first-order languages and structures (03C07) Descriptive complexity and finite models (68Q19)

Cited In (24)

• Testing Simon's congruence
• Deciding \(\mathrm{FO}^2\) alternation for automata over finite and infinite words
• Title not available (Why is that?)
• Bounds for the quantifier depth in finite-variable logics: alternation hierarchy
• Finite-degree predicates and two-variable first-order logic
• On the lattice of sub-pseudovarieties of DA.
• The word problem for omega-terms over the Trotter-Weil hierarchy
• Forbidden Patterns for FO² Alternation Over Finite and Infinite Words
• Expressive power of existential first-order sentences of Büchi's sequential calculus
• The Word Problem for Omega-Terms over the Trotter-Weil Hierarchy
• The half-levels of the \(\mathrm {FO}_2\) alternation hierarchy
• On the strictness of the quantifier structure hierarchy in first-order logic
• On Simon's congruence closure of a string
• Matching patterns with variables under Simon's congruence
• Alternation hierarchies of first order logic with regular predicates
• Simon's congruence pattern matching
• Bounds for the quantifier depth in finite-variable logics: alternation hierarchy
• Alternating complexity of counting first-order logic for the subword order
• On FO 2 Quantifier Alternation over Words
• Conelikes and ranker comparisons
• Structure Theorem and Strict Alternation Hierarchy for FO2 on Words
• Algebraic characterization of the alternation hierarchy in \(\mathrm{FO}^2[<]\) on finite words
• Two variable vs. linear temporal logic in model checking and games
• Title not available (Why is that?)

This page was built for publication: Structure Theorem and Strict Alternation Hierarchy for FO^2 on Words

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3395099)