Arity and alternation in second-order logic
type: Item
instance of: scholarly article
title: Arity and alternation in second-order logic
zbMATH Open document ID: 0854.03006
DOI: 10.1016/0168-0072(95)00013-5
author: Y. B. Pnueli
author: Johann A. Makowsky
published in: Annals of Pure and Applied Logic
publication date: 1996-10-30T00:00:00Z
review text: This paper studies the expressiveness of second-order logic over finite structures. Two hierarchies of second-order formulas are introduced. In the \(\text{AA} (k,n)\) hierarchy the arity of any relation variable is \(\leq k\) and the number of alternations of quantifiers (first or second order) is \(\leq n\). In the \(\text{SAA} (k,n)\) hierarchy all second-order quantifiers come first and the first-order quantifiers are ignored in the alternation count. It is proven that for every \(k\), \(n \in N\) there are problems not definable in \(\text{AA} (k,n)\) but definable in \(\text{AA} (k + c_1, \;n + d_1)\) for some \(c_1\), \(d_1 \in N\). The method of proof involves the introduction of \(\text{AUTOSAT}(F)\), a set of formulas of the fragment of second-order logic \(F\) which satisfy themselves. The authors investigate the complexity of \(\text{AUTOSAT} (F)\) for various \(F\). For example they show that \(\text{AUTOSAT} (FOL)\) is PSpace-complete and for every \(k\), \(n \in N\) \(\text{AUTO(SAA} (k,n))\) is PSpace-complete.
Mathematics Subject Classification ID: 03B15
Mathematics Subject Classification ID: 03D15
Mathematics Subject Classification ID: 68Q15
Mathematics Subject Classification ID: 03C13
zbMATH DE Number: 909720
zbMATH Keywords: expressiveness of second-order logic over finite structures
zbMATH Keywords: hierarchies of second-order formulas
zbMATH Keywords: alternations of quantifiers
zbMATH Keywords: complexity
reviewed by: J. M. Plotkin
describes a project that uses: AUTO
MaRDI profile type: Publication
full work available at URL: 0168-0072(95)00013-5
OpenAlex ID: W2007091370
cites work: Reachability is harder for directed than for undirected finite graphs
cites work: Weak Second‐Order Arithmetic and Finite Automata
cites work: Q2757822
cites work: The monadic second-order logic of graphs. I: Recognizable sets of finite graphs
cites work: Second-order and Inductive Definability on Finite Structures
cites work: A regular characterization of graph languages definable in monadic second-order logic
cites work: Q4525283
cites work: Q5592246
cites work: Q4385525
cites work: Complexity classes and theories of finite models
cites work: Q4395562
cites work: Q4501155
cites work: Classifying regular events in symbolic logic
cites work: On the definability of properties of finite graphs
description: scientific article; zbMATH DE number 909720