First order quantifiers in~monadic second order logic

Keisler, H. Jerome ; Lotfallah, Wafik Boulos

J. Symbolic Logic, Tome 69 (2004) no. 1, p. 118-136 / Harvested from Project Euclid

Résumé

This paper studies the expressive power that an extra first order quantifier adds to a fragment of monadic second order logic, extending the toolkit of Janin and Marcinkowski [JM01]. ¶ We introduce an operation exists_n(S) on properties S that says "there are n components having S". We use this operation to show that under natural strictness conditions, adding a first order quantifier word u to the beginning of a prefix class V increases the expressive power monotonically in u. As a corollary, if the first order quantifiers are not already absorbed in V, then both the quantifier alternation hierarchy and the existential quantifier hierarchy in the positive first order closure of V are strict. ¶ We generalize and simplify methods from Marcinkowski [Mar99] to uncover limitations of the expressive power of an additional first order quantifier, and show that for a wide class of properties S, S cannot belong to the positive first order closure of a monadic prefix class W unless it already belongs to W. ¶ We introduce another operation alt(S) on properties which has the same relationship with the Circuit Value Problem as reach(S) (defined in [JM01]) has with the Directed Reachability Problem. We use alt(S) to show that Π_n⊈ FO(Σ_n), Σ_n⊈ FO(Δ_n), and Δ_n+1⊈ FOB(Σ_n), solving some open problems raised in [Mat98].

Détail

Publié le : 2004-03-14
Classification: