Quantifier alternation in two-variable first-order logic with successor is decidable

DOI10.4230/LIPICS.STACS.2013.305MaRDI QIDQ2957893zbMATH OpenOpenAlexFDO

Authors Manfred Kufleitner, Alexander Lauser

Publication date 30 January 2017

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

zbMATH Keywords

automata theoryfirst-order logicregular languagessemigroups

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44) Automata and formal grammars in connection with logical questions (03D05)

Abstract: We consider the quantifier alternation hierarchy within two-variable first-order logic FO^2[<,suc] over finite words with linear order and binary successor predicate. We give a single identity of omega-terms for each level of this hierarchy. This shows that it is decidable for a given regular language and a non-negative integer m, whether the language is definable by a formula in FO^2[<,suc] which has at most m quantifier alternations. We also consider the alternation hierarchy of unary temporal logic TL[X,F,Y,P] defined by the maximal number of nested negations. This hierarchy coincides with the FO^2[<,suc] alternation hierarchy.

Recommendations

• The \(\mathrm{FO}^2\) alternation hierarchy is decidable
• Alternation hierarchies of first order logic with regular predicates
• The half-levels of the \(\mathrm {FO}_2\) alternation hierarchy
• Going Higher in the First-Order Quantifier Alternation Hierarchy on Words
• Going Higher in First-Order Quantifier Alternation Hierarchies on Words

Cited in

(19)

• Varieties
• The half-levels of the \(\mathrm {FO}_2\) alternation hierarchy
• On logical hierarchies within \(\mathrm{FO}^{2}\)-definable languages
• Bounds for the quantifier depth in finite-variable logics: alternation hierarchy
• Alternation hierarchies of first order logic with regular predicates
• An effective characterization of the alternation hierarchy in two-variable logic
• Bounds for the quantifier depth in finite-variable logics: alternation hierarchy
• Structure Theorem and Strict Alternation Hierarchy for FO^2 on Words
• Structure Theorem and Strict Alternation Hierarchy for FO2 on Words
• scientific article; zbMATH DE number 1775408 (Why is no real title available?)
• Separating regular languages with two quantifiers alternations
• The \(\mathrm{FO}^2\) alternation hierarchy is decidable
• Block products and nesting negations in \(\mathrm{FO}^{2}\)
• The Quantifier Alternation Hierarchy of Synchronous Relations
• One quantifier alternation in first-order logic with modular predicates
• Finite-degree predicates and two-variable first-order logic
• Locality and Centrality: The Variety ZG
• The amazing mixed polynomial closure and its applications to two-variable first-order logic
• Deciding \(\mathrm{FO}^2\) alternation for automata over finite and infinite words

This page was built for publication: Quantifier alternation in two-variable first-order logic with successor is decidable

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