Second-order logic: Difference between revisions

Revision as of 04:37, 8 August 2025

Latest revision as of 11:07, 16 August 2025

Line 135:

== Relation to computational complexity==

{{anchor|Applications to complexity|relation to computational complexity}}

The expressive power of various forms of second-order logic on finite structures is intimately tied to [[computational complexity theory]]. The field of [[descriptive complexity]] studies which computational [[complexity class]]es can be characterized by the power of the logic needed to express languages (sets of finite strings) in them. A string ''w''&nbsp;=&nbsp;''w''₁···''w_n'' in a finite alphabet ''A'' can be represented by a finite structure with ___domain ''D''&nbsp;=&nbsp;{1,...,''n''}, unary predicates ''P_a'' for each ''a''&nbsp;∈&nbsp;''A'', satisfied by those indices ''i'' such that ''w_i''&nbsp;=&nbsp;''a'', and additional predicates that serve to uniquely identify which index is which (typically, one takes the graph of the successor function on ''D'' or the order relation <, possibly with other arithmetic predicates). Conversely, the [[Cayley table]]s of any finite structure (over a finite [[signature (logic)|signature]]) can be encoded by a finite string.

This identification leads to the following characterizations of variants of second-order logic over finite structures:

* REG (the [[regular language]]s) is the set of languages definable by monadic, second-order formulas ([[Büchi-Elgot-Trakhtenbrot theorem]], 1960).

* [[NP (complexity)|NP]] is the set of languages definable by existential, second-order formulas ([[Fagin's theorem]], 1974).

* [[co-NP]] is the set of languages definable by universal, second-order formulas.