記述的複雑性理論

In circuit complexity, first-order logic with arbitrary predicates can be shown to be equal to AC⁰, the first class in the AC hierarchy. Indeed, there is a natural translation from FO's symbols to nodes of circuits, with ${\displaystyle \forall ,\exists }$ being ${\displaystyle \land }$ and ${\displaystyle \lor }$ of size n. First-order logic in a signature with arithmetical predicates characterises the restriction of the AC⁰ family of circuits to those constructible in alternating logarithmic time.^[2] First-order logic in a signature with only the order relation corresponds to the set of star-free languages.^[9][10]

First-order logic gains substantially in expressive power when it is augmented with an operator that computes the transitive closure of a binary relation. The resulting transitive closure logic is known to characterise non-deterministic logarithmic space (NL) on ordered structures. This was used by Immerman to show that NL is closed under complement (i. e. that NL = co-NL).^[11]

When restricting the transitive closure operator to deterministic transitive closure, the resulting logic exactly characterises logarithmic space on ordered structures.

On structures that have a successor function, NL can also be characterised by second-order Krom formulae.

SO-Krom is the set of Boolean queries definable with second-order formulae in conjunctive normal form such that the first-order quantifiers are universal and the quantifier-free part of the formula is in Krom form, which means that the first-order formula is a conjunction of disjunctions, and in each "disjunction" there are at most two variables. Every second-order Krom formula is equivalent to an existential second-order Krom formula.

SO-Krom characterises NL on structures with a successor function.^[12]

FO[LFP]は、単調式の不動点を表す最小不動点演算子による一階述語論理の拡張です。これにより、一階述語論理は再帰を表現する能力を獲得します。ImmermanとVardiによって独立に示されたImmerman –Vardiの定理は、FO[LFP]が順序構造上のPTIMEを特徴づけることを示しています。^{[ 13 ] [ 14 ]}

2025年現在しかし、順序付けされていない構造における PTIME を特徴付ける自然な論理が存在するかどうかは、まだ未解決である。

アビテブール・ヴィアヌの定理によれば、FO[LFP]=FO[PFP]となるのは、FO[LFP]=FO[PFP]となる場合のみであり、したがってP=PSPACEとなる場合のみである。この結果は他の固定点にも拡張されている。^{[ 7 ]}

後継関数が存在する場合、PTIMEは2次ホーン式によって特徴付けられることもあります。

SO-Hornは、SO式を選言標準形で定義できるブールクエリの集合であり、一階述語論理の量化子はすべて全称であり、量化子を含まない部分はHorn形式である。つまり、それはORの大きなANDであり、各「OR」では、おそらく1つを除くすべての変数が否定される。

このクラスは、後継関数を持つ構造ではPと等しい。 ^{[ 15 ]}

これらの式は、存在二階ホーン論理のプレネックス式に変換することができる。^{[ 12 ]}

ロナルド・フェイギンが1974年に、複雑性クラスNPが、存在二階述語論理で公理化可能な構造のクラスによって正確に特徴付けられることを証明したことが、記述的複雑性理論の出発点となった。^{[ 5 ] [ 16 ]}

存在式の補集合は普遍式であるため、co-NPは普遍的な二階述語論理によって特徴づけられることが直ちに導かれる。^{[ 5 ]}

したがって、無制限の2階論理は、多項式階層PHに等しい。より正確には、ファギンの定理の次の一般化が得られる。2階の存在量化子と全称量化子がk回交互に多項式階層のk番目のレベルを特徴付ける、前置正規形の式の集合。^{[ 17 ]}

他のほとんどの複雑性クラスの特徴付けとは異なり、フェイギンの定理とその一般化は、構造上の全順序を前提としていません。これは、存在二階論理自体が、二階変数を使用して構造上の可能な全順序を参照するのに十分な表現力を持っているためです。^{[ 18 ]}

The class of all problems computable in polynomial space, PSPACE, can be characterised by augmenting first-order logic with a more expressive partial fixed-point operator.

Partial fixed-point logic, FO[PFP], is the extension of first-order logic with a partial fixed-point operator, which expresses the fixed-point of a formula if there is one and returns 'false' otherwise.

Partial fixed-point logic characterises PSPACE on ordered structures.^[19]

Second-order logic can be extended by a transitive closure operator in the same way as first-order logic, resulting in SO[TC]. The TC operator can now also take second-order variables as argument. SO[TC] characterises PSPACE. Since ordering can be referenced in second-order logic, this characterisation does not presuppose ordered structures.^[20]

We define higher-order variables. A variable of order ${\displaystyle i>1}$ has an arity ${\displaystyle k}$ and represents any set of ${\displaystyle k}$-tuples of elements of order ${\displaystyle i-1}$. They are usually written in upper-case and with a natural number as exponent to indicate the order. Higher-order logic is the set of first-order formulae where we add quantification over higher-order variables; hence we will use the terms defined in the FO article without defining them again.

HO${\displaystyle ^{i}}$ is the set of formulae with variables of order at most ${\displaystyle i}$. HO$\displaystyle _{j}^{i}}$ is the subset of formulae of the form $\displaystyle \phi =\exists {\overline {X_{1}^{i}}}\forall {\overline {X_{2}^{i}}}\dots Q{\overline {X_{j}^{i}}}\psi }$, where ${\displaystyle Q}$ is a quantifier and ${\displaystyle Q{\overline {X^{i}}}}$ means that ${\displaystyle {\overline {X^{i}}}}$ is a tuple of variable of order ${\displaystyle i}$ with the same quantification. So HO$\displaystyle _{j}^{i}}$ is the set of formulae with ${\displaystyle j}$ alternations of quantifiers of order ${\displaystyle i}$, beginning with ${\displaystyle \exists }$, followed by a formula of order ${\displaystyle i-1}$.

Using the standard notation of the tetration, $\displaystyle \exp _{2}^{0}(x)=x}$ and $\displaystyle \exp _{2}^{i+1}(x)=2^{\exp _{2}^{i}(x)}}$. ${\displaystyle \exp _{2}^{i+1}(x)=2^{2^{2^{2^{\dots ^{2^{x}}}}}}}$ with ${\displaystyle i}$ times ${\displaystyle 2}$

Every formula of order ${\displaystyle i}$th is equivalent to a formula in prenex normal form, where we first write quantification over variable of ${\displaystyle i}$th order and then a formula of order ${\displaystyle i-1}$ in normal form.

HO is equal to the class ELEMENTARY of elementary functions. To be more precise, ${\displaystyle {\mathsf {HO}}_{0}^{i}={\mathsf {NTIME}}(\exp _{2}^{i-2}(n^{O(1)}))}$, meaning a tower of ${\displaystyle (i-2)}$ 2s, ending with ${\displaystyle n^{c}}$, where ${\displaystyle c}$ is a constant. A special case of this is that ${\displaystyle \exists {\mathsf {SO}}={\mathsf {HO}}_{0}^{2}={\mathsf {NTIME}}(n^{O(1)})={\color {Blue}{\mathsf {NP}}}}$, which is exactly Fagin's theorem. Using oracle machines in the polynomial hierarchy, ${\displaystyle {\mathsf {HO}}_{j}^{i}={\color {Blue}{\mathsf {NTIME}}}(\exp _{2}^{i-2}(n^{O(1)})^{\Sigma _{j}^{\mathsf {P}}})}$