1936 LABEL:LastPageJul. 20, 2022Jul. 14, 2023

[a,*] [b,*] [a]

# Capturing the polynomial hierarchy by
second-order revised Krom logic

Kexu Wang  ,  Shiguang Feng0000-0002-5110-3881  and  Xishun Zhao  Institute of
Logic and Cognition, Sun Yat-sen University, Guangzhou, 510275, China  School
of Computer Science and Engineering, Sun Yat-sen University, Guangzhou,
510006, China<EMAIL_ADDRESS>
###### Abstract.

We study the expressive power and complexity of second-order revised Krom
logic (SO-KROMr). On ordered finite structures, we show that its existential
fragment $\Sigma^{1}_{1}$-KROMr equals $\Sigma^{1}_{1}$-KROM, and captures NL.
On all finite structures, for $k\geq 1$, we show that $\Sigma^{1}_{k}$ equals
$\Sigma^{1}_{k+1}$-KROMr if $k$ is even, and $\Pi^{1}_{k}$ equals
$\Pi^{1}_{k+1}$-KROMr if $k$ is odd. The results give an alternative logic to
capture the polynomial hierarchy. We also introduce an extended version of
second-order Krom logic (SO-EKROM). On ordered finite structures, we prove
that SO-EKROM collapses to $\Pi^{1}_{2}$-EKROM and equals $\Pi^{1}_{1}$. Both
SO-EKROM and $\Pi^{1}_{2}$-EKROM capture co-NP on ordered finite structures.

###### Key words and phrases:

polynomial hierarchy, Krom logic, descriptive complexity, second-order logic

Corresponding author: Shiguang Feng.

∗ These authors contributed equally to this work.

## Introduction

Descriptive complexity studies the logical characterization of computational
complexity classes. It describes the property of a problem using the logical
method. Computational complexity considers the computational resources such as
time and space needed to decide a problem, whereas descriptive complexity
explores the minimal logic that captures a complexity class. We say that a
logic $\mathcal{L}$ captures a complexity class $\mathcal{C}$, if (i) the data
complexity of $\mathcal{L}$ is in $\mathcal{C}$, i.e., for every $\mathcal{L}$
formula $\varphi$, the set of models of $\varphi$ is decidable in
$\mathcal{C}$; and (ii) if a class of finite structures is in $\mathcal{C}$,
then it is definable by an $\mathcal{L}$ formula. Moreover, if two logics
$\mathcal{L}_{1}$ and $\mathcal{L}_{2}$ capture two complexity classes
$\mathcal{C}_{1}$ and $\mathcal{C}_{2}$, respectively, then $\mathcal{L}_{1}$
and $\mathcal{L}_{2}$ have the same expressive power if and only if
$\mathcal{C}_{1}$ is equal to $\mathcal{C}_{2}$ [EF95]. So the equivalence
problem between different complexity classes can be transformed into the
expressive power problem of different logics. In 1974, Fagin showed that the
existential fragment of second-order logic ($\exists$SO) captures NP [Fag74].
This seminal work had been followed by many studies in the logical
characterization of complexity classes. In 1982, Immerman and Vardi
independently showed that the least fixed-point logic FO(LFP) captures P on
ordered finite structures [Imm82, Var82]. In 1987, Immerman showed that the
deterministic transitive closure logic FO(DTC) and transitive closure logic
FO(TC) capture L and NL on ordered finite structures, respectively [Imm87]. In
1989, Abiteboul and Vianu showed that the partial fixed-point logic FO(PFP)
captures PSPACE on ordered finite structures [AV89].

Whether P equals NP is an important problem in theoretical computer science.
$\exists$SO captures NP on all finite structures. Hence, no logic capturing P
on all finite structures implies $\mathrm{P}\neq\mathrm{NP}$. The capturing
result of FO(LFP) for P is on ordered structures. Actually, FO(LFP) even
cannot express the parity of a structure [EF95]. So finding a logic that can
capture P effectively on all finite structures is of importance. Many
extensions of FO(LFP) had been studied. FO(IFP, #) is obtained by adding
counting quantifiers to the inflationary fixed-point logic FO(IFP) which has
the same expressive power as FO(LFP) [GO92, Ott96]. FO(IFP,rank) is an
extension of FO(IFP) with the rank operator that can define the rank of a
matrix [Daw08, DGHL09, ABD09]. Both FO(IFP, #) and FO(IFP,rank) are strictly
more expressive than FO(LFP), but neither of them captures P on all finite
structures [EF95, DGP19]. Second-order logic and its fragments are further
candidates of logics for P. In [Grä91], Grädel showed that SO-HORN captures P
on ordered finite structures. Feng and Zhao introduced second-order revised
Horn logic (SO-HORNr) and showed that it equals FO(LFP) on all finite
structures [FZ12, FZ13].

Similar to the results for P, it is easy to check that no logic capturing NL
on all finite structures implies $\mathrm{NL}\neq\mathrm{NP}$. Grädel showed
that SO-KROM captures NL on ordered finite structures [Grä92]. Cook and
Kolokolova introduced the second-order theory V-Krom of bounded arithmetic for
NL that is based on SO-KROM [CK04]. In this paper, we introduce second-order
revised Krom logic (SO-KROMr). It is an extension of SO-KROM by allowing the
formula $\exists\bar{z}R\bar{z}$ in the clauses where $R$ is a second-order
variable. SO-KROMr is strictly more expressive than SO-KROM. Its existential
fragment $\Sigma^{1}_{1}$-KROMr is equivalent to SO-KROM on ordered finite
structures. For all $k\geq 1$, on all finite structures, we show that every
$\Sigma^{1}_{k}$ formula is equivalent to a $\Sigma^{1}_{k+1}$-KROMr formula
for even $k$, and every $\Pi^{1}_{k}$ formula is equivalent to a
$\Pi^{1}_{k+1}$-KROMr formula for odd $k$. Hence, every second-order formula
is equivalent to an SO-KROMr formula. For the data complexity of SO-KROMr, we
show that $\Sigma^{1}_{k+1}$-KROMr is in $\Sigma^{p}_{k}$ for even $k$, and
$\Pi^{1}_{k+1}$-KROMr is in $\Pi^{p}_{k}$ for odd $k$, where
$\Sigma^{p}_{0}=\Pi^{p}_{0}=\mathrm{P}$, $\Sigma^{p}_{k+1}$ is the set of
decision problems solvable in nondeterministic polynomial time by a Turing
machine augmented with an oracle in $\Sigma^{p}_{k}$, and $\Pi^{p}_{k+1}$ is
the complement of $\Sigma^{p}_{k+1}$ [Sto76]. The polynomial time hierarchy
$\mathrm{PH}=\bigcup^{\infty}_{k=0}\Sigma^{p}_{k}$, which is contained within
PSPACE. It is well-known that the second-order formulas $\Sigma^{1}_{k}$
(resp., $\Pi^{1}_{k}$) capture $\Sigma^{p}_{k}$ (resp., $\Pi^{p}_{k}$) ($k\geq
1$) [Imm98]. Combining these we see that SO-KROMr gives an alternative logical
characterization for PH, which is an interesting result in the field of
descriptive complexity. The main results in the paper are summarized in Figure
1.

$\Sigma^{1}_{1}$-KROM$\Sigma^{1}_{2}$$\Sigma^{1}_{4}$$\Sigma^{1}_{2k}$$\dots$$\dots$$\Sigma^{rk}_{1}\equiv\Sigma^{rk}_{2}$$\Sigma^{rk}_{3}\equiv\Sigma^{rk}_{4}$$\Sigma^{rk}_{5}\equiv\Sigma^{rk}_{6}$$\Sigma^{rk}_{2k+1}\equiv\Sigma^{rk}_{2k+2}$NL$\Sigma^{p}_{2}$$\Sigma^{p}_{4}$$\Sigma^{p}_{2k}$$\Pi^{1}_{1}$-KROM$\Pi^{1}_{1}$$\Pi^{1}_{3}$$\Pi^{1}_{2k-1}$$\dots$$\dots$$\Pi^{rk}_{1}$$\Pi^{rk}_{2}\equiv\Pi^{rk}_{3}$$\Pi^{rk}_{4}\equiv\Pi^{rk}_{5}$$\Pi^{rk}_{2k}\equiv\Pi^{rk}_{2k+1}$$\Pi^{p}_{1}$$\Pi^{p}_{3}$$\Pi^{p}_{2k-1}$
Figure 1.  The expressive power and complexity of SO-KROMr. $\Sigma^{rk}_{k}$
and $\Pi^{rk}_{k}$ denote $\Sigma^{1}_{k}$-KROMr and $\Pi^{1}_{k}$-KROMr,
respectively. The dashed rectangle parts show the equivalence relation between
second-order formulas and SO-KROMr formulas. The solid rectangle parts show
the capturing results of SO-KROMr for PH.

The paper is organized as follows. In Section 1, we give the basic definitions
and notations. In Section 2, we study the expressive power and complexity of
the existential fragment of SO-KROMr. In Section 3, we study the descriptive
complexity of SO-KROMr. In Section 4, we introduce second-order extended Krom
logic and study its descriptive complexity. Section 5 is the conclusion of the
paper.

##  1\. Preliminaries

Let
$\tau=\\{\mathbf{c}_{1},\mathbf{c}_{2},\dots,\mathbf{c}_{m},P_{1},P_{2},\dots,P_{n}\\}$
be a vocabulary, where $\mathbf{c}_{1},$ $\mathbf{c}_{2},\dots,\mathbf{c}_{m}$
are constant symbols and $P_{1},P_{2},\dots,P_{n}$ are relation symbols. A
$\tau$-structure $\mathcal{A}$ is a tuple

$\langle
A,\mathbf{c}_{1}^{A},\mathbf{c}_{2}^{A},\dots,\mathbf{c}_{m}^{A},P_{1}^{A},P_{2}^{A},\dots,P_{n}^{A}\rangle,$

where $A$ is the domain of $\mathcal{A}$, and
$\mathbf{c}_{1}^{A},\mathbf{c}_{2}^{A},\dots,\mathbf{c}_{m}^{A}$,
$P_{1}^{A},P_{2}^{A},\dots,P_{n}^{A}$ are the interpretations of the constant
and relation symbols over $A$, respectively. We assume the identity relation
“=” is contained in every vocabulary, and omit the superscript “$A$” in the
notation when no confusion is caused. We call $\mathcal{A}$ finite if its
domain $A$ is a (nonempty) finite set. In this paper, all structures
considered are finite. We use $|\ |$ to denote the cardinality of a set or the
arity of a tuple, e.g., $|\\{a,b,c\\}|=3$ and $|\bar{x}|=3$ where
$\bar{x}=(x_{1},x_{2},x_{3})$, and $arity(X)$ to denote the arity of a
relation symbol (variable) $X$. A finite structure is ordered if it is
equipped with a linear order relation “$\leq$”, a successor relation
“$\mathrm{SUCC}$”, and constants “min” and “max” interpreted as the minimal
and maximal elements, respectively.

Given a logic $\mathcal{L}$, we use $\mathcal{L}(\tau)$ to denote the set of
$\mathcal{L}$ formulas over vocabulary $\tau$. For better readability, the
symbol “$\tau$” is omitted when it is clear from context. Given two logics
$\mathcal{L}_{1}$ and $\mathcal{L}_{2}$, we use
$\mathcal{L}_{1}\leq\mathcal{L}_{2}$ to denote that every $\mathcal{L}_{1}$
formula is equivalent to an $\mathcal{L}_{2}$ formula. If both
$\mathcal{L}_{1}\leq\mathcal{L}_{2}$ and $\mathcal{L}_{2}\leq\mathcal{L}_{1}$
hold, then we write $\mathcal{L}_{1}\equiv\mathcal{L}_{2}$.

Given a vocabulary $\tau$, the second-order Krom logic over $\tau$, denoted by
SO-KROM($\tau$), is a set of second-order formulas of the form

$Q_{1}R_{1}\cdots Q_{m}R_{m}\forall\bar{x}(C_{1}\wedge\cdots\wedge C_{n})$

where each $Q_{i}\in\\{\forall,\exists\\}$, $C_{1},\dots,C_{n}$ are Krom
clauses with respect to $R_{1},\dots,R_{m}$, more precisely, each $C_{j}$ is a
disjunction of the form

$\beta_{1}\vee\cdots\vee\beta_{q}\vee H_{1}\vee H_{2},$

where

  1. (1)

each $\beta_{s}$ for $s\in\\{1,\dots,q\\}$ is either $P\bar{y}$ or $\neg
P\bar{y}$ $(P\in\tau)$;

  2. (2)

each $H_{t}$ is either $R_{i}\,\bar{z}$, $\neg R_{i}\,\bar{z}$ $(1\leq i\leq
m)$, or $\bot$ (for false).

If we replace (2) by

  1. (2′)

each $H_{t}$ is either $R_{i}\,\bar{z}$, $\neg R_{i}\,\bar{z}$, $\exists
z_{1}\cdots\exists z_{arity(R_{i})}\,R_{i}\,z_{1}\dots z_{arity(R_{i})}$
$(1\leq i\leq m)$, or $\bot$ (for false),

then we call this logic second-order revised Krom Logic, denoted by SO-
KROM${}^{r}(\tau)$. We use $\Sigma_{k}^{1}\text{-KROM}^{r}$ (resp.,
$\Pi_{k}^{1}\text{-KROM}^{r}$) to denote the set of SO-KROMr formulas whose
second-order prefix starts with an existential (resp., a universal) quantifier
and alternates $k-1$ times between series of existential and universal
quantifiers.

A directed graph is strongly connected iff there exists a path between every
pair of nodes. The strong connectivity problem is NL-complete, which is
defined by

Input:

a directed graph $G=(V,E)$,

Output:

yes if $G$ is strongly connected, and no otherwise.

Since $\mathrm{NL}=\mathrm{co\text{-}NL}$, the complement of the strong
connectivity problem is also NL-complete, which can be defined by the
following $\Sigma_{1}^{1}\text{-KROM}^{r}$ formula

$\exists R\exists Y\forall x\forall y\forall
z\left(\begin{array}[]{l}(Exy\rightarrow Rxy)\wedge(Exy\wedge Ryz\rightarrow
Rxz)\\\ \wedge(\neg Rxy\leftrightarrow Yxy)\wedge\exists u\exists
vYuv\end{array}\right)$

where $R$ is the transitive closure of $E$, and $Y$ is the complement of $R$.
A graph $G$ satisfies the formula iff there exist two nodes $a,b$ such that
$a$ cannot reach $b$.

SO-KROM is closed under substructures [Grä92], which means that if a structure
satisfies a SO-KROM formula then all its substructures also satisfy the
formula. Because a non-strongly connected graph may be made strongly connected
by removing nodes, SO-KROM cannot define the complement of the strong
connectivity problem. The above example shows that SO-KROMr is strictly more
expressive than SO-KROM.

##  2\. The expressive power and complexity of $\Sigma_{1}^{1}$-KROMr

In this section, we study the expressive power of the universal and
existential fragments of SO-KROMr, and show that $\Sigma_{1}^{1}$-KROMr
captures NL on finite ordered structures.

######  Proposition 1.

Every $\Pi^{1}_{1}\text{-}\mathrm{KROM}^{r}$ formula is equivalent to a first-
order formula $\forall\bar{x}\varphi$, where $\varphi$ is a quantifier-free
$\mathrm{CNF}$ formula.

######  Proof 2.1.

Given a $\Pi^{1}_{1}$-KROMr formula $\Phi=\forall X_{1}\dots\forall
X_{n}\forall\bar{x}(C_{1}\wedge\dots\wedge C_{m})$, we deal with each clause
$C_{j}$ for $j\in\\{1,\dots,m\\}$ as follows. Let $\alpha$ denote the first-
order part of $C_{j}$.

Case 1:

If $C_{j}=\alpha\vee\neg
X_{i}\bar{x}_{1}\vee\exists\bar{x}_{2}X_{i}\bar{x}_{2}$, then remove the
clause $C_{j}$.

Case 2:

If $C_{j}=\alpha\vee X_{i}\bar{x}_{1}\vee\neg X_{i}\bar{x}_{2}$, then replace
$C_{j}$ by $\alpha\vee\bar{x}_{1}=\bar{x}_{2}$.

Case 3:

For the other cases, remove all occurrences of second-order variables in
$C_{j}$.

After the above steps, all second-order variables are removed and we obtain a
first-order formula $\phi=\forall\bar{x}(C_{1}^{\prime}\wedge\dots\wedge
C_{m^{\prime}}^{\prime})$, where each $C_{j}^{\prime}$ is quantifier-free.

In Case 1, $\neg X_{i}\bar{x}_{1}\vee\exists\bar{x}_{2}X_{i}\bar{x}_{2}$ is a
tautology, so the clause can be removed safely. In Case 2, if
$\bar{x}_{1}=\bar{x}_{2}$, then $X_{i}\bar{x}_{1}\vee\neg X_{i}\bar{x}_{2}$ is
always true; if $\bar{x}_{1}\neq\bar{x}_{2}$, then there exists a valuation
for $X_{i}$ such that $X_{i}\bar{x}_{1}\vee\neg X_{i}\bar{x}_{2}$ is false,
the clause is true iff $\alpha$ is true. Hence, $\forall
X_{i}\forall\bar{x}(\alpha\vee X_{i}\bar{x}_{1}\vee\neg X_{i}\bar{x}_{2})$ is
equivalent to $\forall\bar{x}(\alpha\vee\bar{x}_{1}=\bar{x}_{2})$. In Case 3,
there is always a valuation for the second-order variables in $C_{j}$ under
which the second-order part of $C_{j}$ is false. So all occurrences of second-
order variables can be removed from $C_{j}$. Therefore, $\Phi$ and $\phi$ are
equivalent.

######  Corollary 2.

For each $k\geq 1$, if $k$ is odd, then
$\Sigma^{1}_{k}\text{-}\mathrm{KROM}^{r}\equiv\Sigma^{1}_{k+1}\textbf{-}\mathrm{KROM}^{r}$;
and if $k$ is even, then
$\Pi^{1}_{k}\text{-}\mathrm{KROM}^{r}\equiv\Pi^{1}_{k+1}\text{-}\mathrm{KROM}^{r}$.

######  Proof 2.2.

If the type of the innermost second-order quantifier block of a SO-KROMr
formula is universal, then it can be removed by Proposition 1 to get an
equivalent formula.

We use $\varphi[\alpha/\beta]$ to denote replacing the variable (or the
formula) $\alpha$ in $\varphi$ with $\beta$.

######  Lemma 3.

Let $\exists x_{1}\dots\exists x_{n}\phi$ be a quantified Boolean formula. It
is equivalent to the following formula

$\phi[x_{1}/\bot,\dots,x_{n}/\bot]\vee\bigvee_{1\leq i\leq n}\exists
x_{1}\dots\exists x_{i-1}\exists x_{i+1}\dots\exists x_{n}\phi[x_{i}/\top].$

######  Proof 2.3.

$\exists x_{1}\dots\exists x_{n}\phi$ is true iff $\phi$ is true when all
$x_{1},\dots,x_{n}$ are false, or for some $x_{i}$, where $(1\leq i\leq n)$,
the formula $\exists x_{1}\dots\exists x_{i-1}\exists x_{i+1}\dots\exists
x_{n}\phi$ is true when $x_{i}$ is true.

From Lemma 3 we can infer the following proposition.

######  Proposition 4.

Every $\Sigma^{1}_{1}\text{-}\mathrm{KROM}^{r}$ formula is equivalent to a
formula of the form
$\exists\bar{y}_{1}\phi_{1}\vee\dots\vee\exists\bar{y}_{n}\phi_{n}$, where
each $\phi_{i}$ for $i\in\\{1,\dots,n\\}$ is a
$\Sigma^{1}_{1}\text{-}\mathrm{KROM}$ formula.

######  Proof 2.4.

Let $\Psi=\exists R\exists\mskip
1.5mu\overline{\mskip-1.5mu{Y}\mskip-1.5mu}\mskip 1.5mu\forall\bar{x}\phi$ be
a $\Sigma^{1}_{1}$-KROMr formula, and $\alpha(\bar{z})=(\bar{z}=\bar{y})\vee
R\bar{z}$ where $\bar{y}$ have no occurrence in $\phi$. It is easily seen that
if $\bar{z}=\bar{y}$ holds then $\alpha(\bar{z})$ is true, and if
$\bar{z}\neq\bar{y}$ holds then $\alpha(\bar{z})$ is equivalent to $R\bar{z}$.
So $\alpha(\bar{z})$ is equivalent to $R\bar{z}$ except at the point
$\bar{y}$. Define

$\Psi^{\prime}=\exists\mskip 1.5mu\overline{\mskip-1.5mu{Y}\mskip-1.5mu}\mskip
1.5mu\forall\bar{x}\phi[R\bar{z}/\bot]\vee\exists\bar{y}\exists R\exists\mskip
1.5mu\overline{\mskip-1.5mu{Y}\mskip-1.5mu}\mskip
1.5mu\forall\bar{x}\phi[R\bar{z}/\alpha(\bar{z})].$

We show that $\Psi$ and $\Psi^{\prime}$ are equivalent. It is easily seen that
for any structure $\mathcal{A}$, $\mathcal{A}\models\Psi$ iff
$(\mathcal{A},R)\models\exists\mskip
1.5mu\overline{\mskip-1.5mu{Y}\mskip-1.5mu}\mskip 1.5mu\forall\bar{x}\phi$,
where either $R=\emptyset$ or $R$ is not empty. Every occurrence of
$\exists\bar{z}R\bar{z}$ in $\Psi^{\prime}$ is either replaced by
$\exists\bar{z}\bot$ or replaced by $\exists\bar{z}\alpha(\bar{z})$ which is a
tautology. We remove the occurrences of $\exists\bar{z}\bot$ and the clauses
containing $\exists\bar{z}\alpha(\bar{z})$ in $\Psi^{\prime}$. For any
structure $\mathcal{A}$, we can construct a quantified Boolean formula
$\Psi_{\mathcal{A}}$ such that $\mathcal{A}\models\Psi$ iff
$\Psi_{\mathcal{A}}$ is true (see the proof of Proposition 9 for details of
the construction). Similarly, we can construct $\Psi^{\prime}_{\mathcal{A}}$
such that $\mathcal{A}\models\Psi^{\prime}$ iff $\Psi^{\prime}_{\mathcal{A}}$
is true. By Lemma 3, $\Psi_{\mathcal{A}}$ and $\Psi^{\prime}_{\mathcal{A}}$
are equivalent. Therefore, $\Psi$ and $\Psi^{\prime}$ are equivalent. The same
procedure can be repeated for each $Y_{i}\in\mskip
1.5mu\overline{\mskip-1.5mu{Y}\mskip-1.5mu}\mskip 1.5mu$ until all occurrences
of $\exists\bar{v}Y_{i}\bar{v}$ are removed. Finally, we can obtain an
equivalent formula of the form
$\exists\bar{y}_{1}\phi_{1}\vee\dots\vee\exists\bar{y}_{n}\phi_{n}$, where
each $\phi_{i}$ $(1\leq i\leq n)$ is a $\Sigma^{1}_{1}$-KROM formula.

######  Proposition 5.

The data complexity of $\Sigma^{1}_{1}\text{-}\mathrm{KROM}^{r}$ is in
$\mathrm{NL}$.

######  Proof 2.5.

By Proposition 4, we only need to show that the data complexity of the formula
$\exists\bar{y}_{1}\phi_{1}\vee\dots\vee\exists\bar{y}_{n}\phi_{n}$, where
each $\phi_{i}$ $(1\leq i\leq n)$ is a $\Sigma^{1}_{1}$-KROM formula, is in
NL. Given a structure $\mathcal{A}$, the Turing machine can
nondeterministically choose an $i\in\\{1,\dots,n\\}$ and a tuple
$\bar{u}_{i}\in A^{|\bar{y}_{i}|}$ in logarithmic space. Whether
$\mathcal{A}\models\phi_{i}[\bar{u}_{i}]$ holds can be checked in NL since the
data complexity of $\Sigma^{1}_{1}$-KROM is in NL [Grä92].

Every $\Sigma^{1}_{1}$-KROM formula is also a $\Sigma^{1}_{1}$-KROMr formula.
Because $\Sigma^{1}_{1}$-KROM captures NL on ordered finite structures
[Grä92], combining Corollary 2 we obtain the following corollary.

######  Corollary 6.

Both $\Sigma^{1}_{1}\text{-}\mathrm{KROM}^{r}$ and
$\Sigma^{1}_{2}\text{-}\mathrm{KROM}^{r}$ capture $\mathrm{NL}$ on ordered
finite structures.

##  3\. The descriptive complexity of SO-KROMr

SO-KROM collapses to its existential fragment. This is unlikely to be true for
SO-KROMr by the following result. Let $\Sigma_{k}$-CNF (resp.,
$\Sigma_{k}$-DNF) denote the set of quantified Boolean formulas
$\exists\bar{x}_{1}\forall\bar{x}_{2}\exists\bar{x}_{3}\dots
Q_{k}\bar{x}_{k}\phi$ whose prefix starts with an existential quantifier and
has $k-1$ alternations between series of existential and universal
quantifiers, and the matrix $\phi$ is a quantifier-free formula in conjunctive
normal form (resp., disjunctive normal form). The definitions for
$\Pi_{k}$-CNF and $\Pi_{k}$-DNF are similar where the formula’s prefix starts
with a universal quantifier. Given a set $\mathbf{F}$ of quantified Boolean
formulas, the evaluation problem of $\mathbf{F}$ is deciding the truth value
of the formulas in it. For the polynomial hierarchy, it is shown that the
evaluation problem of $\Sigma_{k}$-CNF (resp., $\Sigma_{k}$-DNF) is
$\Sigma^{p}_{k}$-complete if $k$ is odd (resp., even) [Sto76]. Hence, the
evaluation problem of $\Pi_{k}$-DNF (resp., $\Pi_{k}$-CNF) is
$\Pi^{p}_{k}$-complete if $k$ is odd (resp., even) by duality.

######  Proposition 7.

The evaluation problem of $\Sigma_{k}\text{-}\mathrm{DNF}$ is definable in
$\Sigma_{k+1}^{1}\text{-}\mathrm{KROM}^{r}$ if $k$ is even, and the evaluation
problem of $\Pi_{k}\text{-}\mathrm{DNF}$ is definable in
$\Pi_{k+1}^{1}\text{-}\mathrm{KROM}^{r}$ if $k$ is odd.

######  Proof 3.1.

We only prove for $\Sigma_{k}$-DNF where $k$ is even, the proof for
$\Pi_{k}$-DNF where $k$ is odd is the same as it. Let vocabulary
$\tau=\\{\mathrm{Clause},\mathrm{Var}_{1},\dots,\mathrm{Var}_{k},\mathrm{Pos},\mathrm{Neg}\\}$,
where $\mathrm{Clause}$, $\mathrm{Var}_{1},\dots,\mathrm{Var}_{k}$ are unary
relation symbols, and $\mathrm{Pos},\mathrm{Neg}$ are binary relation symbols.
Using a similar method as in [Imm98], we can encode a $\Sigma_{k}$-DNF formula
$\exists\bar{x}_{1}\forall\bar{x}_{2}\cdots\exists\bar{x}_{k-1}\forall\bar{x}_{k}\phi$
via a $\tau$-structure $\mathcal{A}$ such that for any $i,j\in A$,
$\mathrm{Clause}\,i$ holds iff $i$ is a clause, $\mathrm{Var}_{h}\,j$ holds
iff $j$ is a variable occurring in the quantifier block
$\exists(\forall)\bar{x}_{h}$ for $h\in\\{1,\dots,k\\}$, and
$\mathrm{Pos}\,ij$ (resp., $\mathrm{Neg}\,ij$) holds iff variable $j$ occurs
positively (resp., negatively) in clause $i$. For example, the
$\Sigma_{4}$-DNF formula

$\exists x_{1}\forall x_{2}\exists x_{3}\forall
x_{4}(\underbrace{(x_{1}\wedge\neg x_{2})}_{1}\vee\underbrace{(x_{2}\wedge\neg
x_{4})}_{2}\vee\underbrace{(x_{3}\wedge x_{4})}_{3})$

can be encoded via the structure
$\langle\\{1,2,3,4\\},\mathrm{Clause},\mathrm{Var}_{1},\mathrm{Var}_{2},\mathrm{Var}_{3},\mathrm{Var}_{4},\mathrm{Pos},\mathrm{Neg}\rangle$,
where $\mathrm{Clause}=\\{1,2,3\\}$, $\mathrm{Var}_{1}=\\{1\\}$,
$\mathrm{Var}_{2}=\\{2\\}$, $\mathrm{Var}_{3}=\\{3\\}$,
$\mathrm{Var}_{4}=\\{4\\}$, $\mathrm{Neg}=\\{(1,2),(2,4)\\}$,
$\mathrm{Pos}=\\{(1,1),(2,2),(3,3),(3,4)\\}$. Let $\Phi$ be the following
formula

$\exists X_{1}\forall X_{2}\dots\exists X_{k-1}\forall X_{k}\exists Y\forall
x\forall y\left(\begin{array}[]{l}\exists
zYz\wedge(Yx\rightarrow\mathrm{Clause}\,x)\wedge\\\ \bigwedge_{1\leq h\leq
k}(Yx\wedge\mathrm{Pos}\,xy\wedge\mathrm{Var}_{h}\,y\rightarrow
X_{h}\,y)\wedge\\\ \bigwedge_{1\leq h\leq
k}(Yx\wedge\mathrm{Neg}\,xy\wedge\mathrm{Var}_{h}\,y\rightarrow\neg
X_{h}\,y)\end{array}\right).$

Obviously, $\Phi$ is a $\Sigma_{k+1}^{1}$-KROMr formula, and it expresses that
there is a valuation $X_{1}$ to $\bar{x}_{1}$, for any valuation $X_{2}$ to
$\bar{x}_{2},\dots$, there is a valuation $X_{k-1}$ to $\bar{x}_{k-1}$, for
any valuation $X_{k}$ to $\bar{x}_{k}$, there is a nonempty set $Y$ of clauses
such that every literal in the clauses in $Y$ is true under the valuation. For
an arbitrary $\Sigma_{k}$-DNF formula $\psi$, let $\mathcal{A}$ be the
$\tau$-structure that encodes $\psi$, it is easily seen that
$\mathcal{A}\models\Phi$ iff $\psi$ is true.

Before showing that every second-order formula is equivalent to a SO-KROMr
formula, we first prove a lemma.

######  Lemma 8.

Every first-order formula is equivalent to a second-order formula $\exists
Y\forall\bar{x}(\exists\bar{y}Y\bar{z}\bar{y}\wedge C_{1}\wedge\cdots\wedge
C_{m})$ where each $C_{i}$ is a disjunction of atomic or negated atomic
formulas.

######  Proof 3.2.

Given a first-order formula $\varphi$, without loss of generality, assume that
$\varphi$ is in the prenex normal form
$\forall\bar{x}_{1}\exists\bar{y}_{1}\cdots\forall\bar{x}_{n}\exists\bar{y}_{n}(C_{1}\wedge\cdots\wedge
C_{m})$, where each $C_{i}$ for $i\in\\{1,\dots,m\\}$ is a disjunction of
atomic or negated atomic formulas. Define

$\begin{array}[]{cl}\varphi_{1}=&\forall\bar{x}_{1}\cdots\forall\bar{x}_{n}\exists\bar{y}_{1}\cdots\exists\bar{y}_{n}Y\bar{x}_{1}\cdots\bar{x}_{n}\bar{y}_{1}\cdots\bar{y}_{n},\\\
\\\
\varphi_{2}=&\forall\bar{x}_{1}\cdots\forall\bar{x}_{n}\forall\bar{y}_{1}\cdots\forall\bar{y}_{n}\forall\bar{x}_{1}^{\prime}\cdots\forall\bar{x}_{n}^{\prime}\forall\bar{y}_{1}^{\prime}\cdots\forall\bar{y}_{n}^{\prime}\\\
&\biggl{(}Y\bar{x}_{1}\cdots\bar{x}_{n}\bar{y}_{1}\cdots\bar{y}_{n}\wedge
Y\bar{x}_{1}^{\prime}\cdots\bar{x}_{n}^{\prime}\bar{y}_{1}^{\prime}\cdots\bar{y}_{n}^{\prime}\\\
&\rightarrow\bigwedge_{1\leq i\leq n}\Bigl{(}(\bigwedge_{1\leq j\leq
i}\bar{x}_{j}=\bar{x}_{j}^{\prime})\rightarrow\bar{y}_{i}=\bar{y}_{i}^{\prime}\Bigr{)}\biggr{)},\\\
\\\
\varphi_{3}=&\forall\bar{x}_{1}\forall\bar{y}_{1}\cdots\forall\bar{x}_{n}\forall\bar{y}_{n}(Y\bar{x}_{1}\cdots\bar{x}_{n}\bar{y}_{1}\cdots\bar{y}_{n}\rightarrow\bigwedge_{1\leq
i\leq m}C_{i}).\end{array}$

The relation $Y$ encodes a Skolem function for each $\bar{y}_{i}$ $(1\leq
i\leq n)$, whose value only depends on the values of
$\bar{x}_{1},\dots,\bar{x}_{i}$. It is easy to check that $\varphi$ is
equivalent to the formula $\exists
Y(\varphi_{1}\wedge\varphi_{2}\wedge\varphi_{3})$, which can be converted to
the form of $\exists Y\forall\bar{x}(\exists\bar{y}Y\bar{z}\bar{y}\wedge
C_{1}\wedge\cdots\wedge C_{m})$, where $\bar{z}$ are variables from $\bar{x}$.

######  Proposition 9.

Every second-order formula is equivalent to an
$\mathrm{SO}\text{-}\mathrm{KROM}^{r}$ formula. More precisely, for each
$k\geq 1$, if $k$ is even, then
$\Sigma^{1}_{k}\leq\Sigma^{1}_{k+1}\text{-}\mathrm{KROM}^{r}$; and if $k$ is
odd, then $\Pi^{1}_{k}\leq\Pi^{1}_{k+1}\text{-}\mathrm{KROM}^{r}$.

######  Proof 3.3.

Given a $\Sigma^{1}_{k}$-formula $\exists X_{1}\forall X_{2}\dots\exists
X_{k-1}\forall X_{k}\varphi$, where $k$ is even and $\varphi$ does not contain
second-order quantifiers, we show that it is equivalent to a
$\Sigma^{1}_{k+1}$-KROMr formula. The proof for the other cases is essentially
the same. By Lemma 8, $\neg\varphi$ is equivalent to a formula $\exists
X_{k+1}\forall\bar{x}(\exists\bar{y}X_{k+1}\bar{z}\bar{y}\wedge
C_{1}\wedge\cdots\wedge C_{m})$. So $\exists X_{1}\forall X_{2}\dots\exists
X_{k-1}\forall X_{k}\varphi$ is equivalent to the formula

$\Phi=\exists X_{1}\forall X_{2}\dots\exists X_{k-1}\forall X_{k}\forall
X_{k+1}\exists\bar{x}(\forall\bar{y}\neg X_{k+1}\bar{z}\bar{y}\vee
D_{1}\vee\cdots\vee D_{m})$

where each $D_{j}$ is a conjunction of atomic (or negated atomic) formulas.
Suppose that $\Phi$ is over vocabulary $\sigma$. Given a $\sigma$-structure
$\mathcal{A}$, we construct a $\Sigma_{k}$-DNF quantified Boolean formula
$\psi$ such that $\mathcal{A}\models\Phi$ iff $\psi$ is true. Let $A$ be the
domain of $\mathcal{A}$. We replace the first-order part
$\exists\bar{x}(\forall\bar{y}\neg Y\bar{z}\bar{y}\vee D_{1}\vee\cdots\vee
D_{m})$ by

$\bigvee_{\bar{a}\in A^{|\bar{x}|}}\biggl{(}\Bigl{(}\bigwedge_{\bar{b}\in
A^{|\bar{y}|}}\neg Y\bar{z}\bar{y}[\bar{y}/\bar{b}]\Bigr{)}\vee
D_{1}\vee\cdots\vee D_{m}\biggr{)}[\bar{x}/\bar{a}].$

We remove the clauses with a formula $(\neg)R\bar{c}$ that is false in
$\mathcal{A}$ and delete the formulas $(\neg)R\bar{c}$ that are true in
$\mathcal{A}$ in every clause, where $R\in\sigma$. Then we replace each
quantifier $\exists X_{i}$ (or $\forall X_{i}$) with a sequence $\exists
X_{i}\bar{d}_{1}\dots\exists X_{i}\bar{d}_{|A|^{arity(X_{i})}}$ (or $\forall
X_{i}\bar{d}_{1}\dots\forall X_{i}\bar{d}_{|A|^{arity(X_{i})}}$) where each
$\bar{d}_{j}\in A^{arity(X_{i})}$. We treat the atoms $X_{i}\bar{d}_{j}$ as
propositional variables, and the resulting formula $\psi$ is a
$\Sigma^{1}_{k}$-DNF quantified Boolean formula. It is clear that
$\mathcal{A}\models\Phi$ iff $\psi$ is true.

By Proposition 7 and its proof, we know that $\psi$ can be encoded in a
$\tau$-structure $\mathcal{B}$, where
$\tau=\langle\mathrm{Clause},\mathrm{Var}_{1},\dots,\mathrm{Var}_{k},\mathrm{Pos},\mathrm{Neg}\rangle$
and there is a $\Sigma_{k+1}^{1}$-KROM${}^{r}(\tau)$ formula $\Psi$ such that
$\psi$ is true iff $\mathcal{B}\models\Psi$. In the following, we define a
quantifier-free interpretation

$\Pi=\Bigl{(}\pi_{\mathrm{uni}}(\bar{v}),\pi_{\mathrm{Clause}}(\bar{v}),\pi_{\mathrm{Var}_{1}}(\bar{v}),\dots,\pi_{\mathrm{Var}_{k}}(\bar{v}),\pi_{\mathrm{Pos}}(\bar{v}_{1},\bar{v}_{2}),\pi_{\mathrm{Neg}}(\bar{v}_{1},\bar{v}_{2})\Bigr{)}$

of $\tau$ in $\sigma$, where
$\pi_{\mathrm{uni}},\pi_{\mathrm{Clause}},\pi_{\mathrm{Var}_{1}},\dots,\pi_{\mathrm{Var}_{k}},\pi_{\mathrm{Pos}},\pi_{\mathrm{Neg}}$
are all quantifier-free formulas over $\sigma$. Intuitively,
$\pi_{\mathrm{uni}}$ defines the domain of $\mathcal{B}$,
$\pi_{\mathrm{Clause}}$ defines the set of clauses of $\psi$, each
$\pi_{\mathrm{Var}_{i}}$ $(1\leq i\leq k)$ defines the set of variables
occurring in the quantifier block $\exists(\forall)X_{i}$,
$\pi_{\mathrm{Pos}}$ (or $\pi_{\mathrm{Neg}}$) defines a variable occurs
positively (or negatively) in a clause.

For any $\sigma$-structure $\mathcal{A}$, $\Pi$ defines a $\tau$-structure
$\mathcal{A}^{\Pi}$ that encodes the formula $\psi$ such that
$\mathcal{A}^{\Pi}\models\Psi$ iff $\psi$ is true iff
$\mathcal{A}\models\Phi$. Since $\Pi$ is an interpretation of $\tau$ in
$\sigma$, we can construct a $\Sigma_{k+1}^{1}$-KROM${}^{r}(\sigma)$ formula
$\Psi^{-\Pi}$ from $\Psi$ such that $\mathcal{A}^{\Pi}\models\Psi$ iff
$\mathcal{A}\models\Psi^{-\Pi}$. Therefore, $\Psi^{-\Pi}$ and $\Phi$ are
equivalent. For more details of the interpretation from one vocabulary to
another, we refer the reader to [EF95].

We suppose that $\mathcal{A}$ contains at least two different elements. Let

$\displaystyle g=\max\\{arity(X_{1}),\dots,arity(X_{k}),arity(X_{k+1}))\\},$
$\displaystyle d=3+\max\\{(|\bar{x}|+m+1),(g+k+1)\\}.$

Define the width of $\Pi$ to be $d$. Let
$\pi_{\mathrm{uni}}(\bar{v})=\bigwedge^{d}_{i=1}(v_{i}=v_{i})$, it defines the
domain of $\mathcal{A}^{\Pi}$. For any $\bar{a}=(a_{1},a_{2},\dots,a_{d})\in
A^{d}$, we will make the following assumptions:

  * •

if $\bar{a}$ encodes a clause, then $a_{1}\neq a_{3}\wedge a_{2}=a_{3}$, and

  * •

if $\bar{a}$ encodes a variable, then $a_{1}\neq a_{3}\wedge a_{1}=a_{2}$.

If $\bar{a}$ encodes a clause, it is partitioned as follows

$\underset{a_{2}=a_{3}}{\underbrace{a_{1}a_{2}a_{3}}}\underset{m+1}{\underbrace{a_{4}\cdots
a_{m+4}}}\underset{|\bar{x}|}{\underbrace{a_{m+5}\cdots
a_{m+4+|\bar{x}|}}}\underset{\text{padding
elements}}{\underbrace{a_{m+5+|\bar{x}|}\cdots a_{d}}}$

where $a_{1}\neq a_{3},a_{2}=a_{3}$, and $a_{m+5},\dots,a_{m+4+|\bar{x}|}$ are
interpretations for $\bar{x}$. $a_{4},\dots,a_{m+4}$ are used to encode the
clauses $\forall\bar{y}\neg X_{k+1}\bar{z}\bar{y}$, $D_{1},\dots,D_{m}$. More
precisely, we use $a_{1}=a_{4}\wedge\bigwedge_{5\leq j\leq m+4}a_{3}=a_{j}$ to
indicate that $\bar{a}$ encodes the clause $\forall\bar{y}\neg
X_{k+1}\bar{z}\bar{y}$, and use $\bigwedge_{4\leq j\leq
i+4}a_{1}=a_{j}\wedge\bigwedge_{i+5\leq h\leq m+4}a_{3}=a_{h}$ to indicate
that $\bar{a}$ encodes $D_{i}$ for $i\in\\{1,\dots,m\\}$, respectively. This
can be expressed by the formula

$\biggl{(}v_{1}=v_{4}\wedge\bigwedge_{5\leq j\leq
m+4}v_{3}=v_{j}\biggr{)}\vee\bigvee_{1\leq i\leq m}\biggl{(}\bigwedge_{4\leq
j\leq i+4}v_{1}=v_{j}\wedge\bigwedge_{i+5\leq h\leq m+4}v_{3}=v_{h}\biggr{)}.$
(1)

We also require that there is no formula that is false in clause $D_{i}$
$(1\leq i\leq m)$, when $\bar{x}$ are interpreted by $a_{m+5}\cdots
a_{m+4+|\bar{x}|}$. Let $\alpha_{i}$ denote the first-order part of $D_{i}$.
This is can be expressed by the formula

$\bigvee_{1\leq i\leq m}\biggl{(}\Bigl{(}\bigwedge_{4\leq j\leq
i+4}v_{1}=v_{j}\wedge\bigwedge_{i+5\leq h\leq
m+4}v_{3}=v_{h}\Bigr{)}\rightarrow\alpha_{i}[\bar{x}/v_{m+5}\cdots
v_{m+4+|\bar{x}|}]\biggr{)}.$ (2)

All padding elements must equal $a_{1}$, which can be expressed by

$v_{1}\neq v_{3}\wedge v_{2}=v_{3}\wedge\bigwedge_{m+5+|\bar{x}|\leq i\leq
d}v_{1}=v_{i}$ (3)

Define $\pi_{\mathrm{Clause}}(\bar{v})$ to be the conjunction of (1), (2) and
(3).

If $\bar{a}$ encodes a variable, it is partitioned as follows

$\underset{a_{1}=a_{2}}{\underbrace{a_{1}a_{2}a_{3}}}\underset{k+1}{\underbrace{a_{4}\cdots
a_{k+4}}}\underset{artiy(X_{i})}{\underbrace{a_{k+5}\cdots
a_{k+4+arity(X_{i})}}}\underset{\text{padding
elements}}{\underbrace{a_{k+5+arity(X_{i})}\cdots a_{d}}}$

where $a_{1}\neq a_{3},a_{1}=a_{2}$, and $a_{4}\cdots a_{k+4}$ encode
$X_{1},\dots,X_{k+1}$. More precisely, we use $\bigwedge_{4\leq j\leq
i+3}a_{1}=a_{j}\wedge\bigwedge_{i+4\leq h\leq k+4}a_{3}=a_{h}$ to indicate
that $\bar{a}$ encodes the variable with relation symbol $X_{i}$, where
$(1\leq i\leq k+1)$. This can be expressed by the following formula

$\mathrm{Var}_{i}(\bar{v})=\biggl{(}\bigwedge_{4\leq j\leq
i+3}v_{1}=v_{j}\wedge\bigwedge_{i+4\leq h\leq k+4}v_{3}=v_{h}\biggr{)}.$

We use $a_{k+5}\cdots a_{k+4+arity(X_{i})}$ to indicate that $\bar{a}$ encodes
the atom $X_{i}a_{k+5}\cdots a_{k+4+arity(X_{i})}$. We also require that all
padding elements $a_{k+5+arity(X_{i})}\cdots a_{d}$ equal $a_{1}$. The formula
$\pi_{\mathrm{Var}_{i}}(\bar{v})$, for $i\in\\{1,\dots,k-1\\}$, is defined by

$\pi_{\mathrm{Var}_{i}}(\bar{v})=\biggl{(}v_{1}\neq v_{3}\wedge
v_{1}=v_{2}\wedge\mathrm{Var}_{i}(\bar{v})\wedge\bigwedge_{k+5+arity(X_{i})\leq
j\leq d}v_{1}=v_{j}\biggr{)}.$

Define $\pi_{V_{k}}(\bar{v})$ to be the conjunction of $v_{1}\neq v_{3}\wedge
v_{1}=v_{2}$ and

$\biggl{(}\mathrm{Var}_{k}(\bar{v})\wedge\bigwedge_{k+5+arity(X_{k})\leq j\leq
d}v_{1}=v_{j}\biggr{)}\vee\biggl{(}\mathrm{Var}_{k+1}(\bar{v})\wedge\bigwedge_{k+5+arity(X_{k+1})\leq
j\leq d}v_{1}=v_{j}\biggr{)}.$

In the following we define the formula
$\pi_{\mathrm{Pos}}(\bar{v}_{1},\bar{v}_{2})$, which expresses that the atom
encoded by $\bar{v}_{2}$ occurs positively in clause $D_{j}$ $(1\leq j\leq m)$
encoded by $\bar{v}_{1}$. Let $\bar{v}_{1}=v_{1,1}\dots v_{1,d}$ and
$\bar{v}_{2}=v_{2,1}\dots v_{2,d}$. We use the following formula
$\varphi_{D_{j}}(\bar{v}_{1})$ to express that $\bar{v}_{1}$ encodes clause
$D_{j}$ for $j\in\\{1,\dots,m\\}$.

$\varphi_{D_{j}}(\bar{v}_{1})=\biggl{(}\pi_{\mathrm{Clause}}(\bar{v}_{1})\wedge\Bigl{(}\bigwedge_{4\leq
l\leq j+4}v_{1,1}=v_{1,l}\wedge\bigwedge_{j+5\leq h\leq
m+4}v_{1,3}=v_{1,h}\Bigr{)}\biggr{)}.$

Suppose that the atomic formula $X_{i}\bar{x}^{\prime}$ occurs in clause
$D_{j}$, where $\bar{x}^{\prime}=x_{1}^{\prime}\dots
x_{arity(X_{i})}^{\prime}$ are variables from $\bar{x}$, and $\bar{v}_{2}$
encodes the atom $X_{i}\bar{v}_{2}^{\prime}$ where $\bar{v}_{2}^{\prime}$ are
the corresponding elements in $\bar{v}_{2}$ by its definition. Let
$\bar{v}_{1}^{\prime}$ be obtained by replacing $\bar{x}^{\prime}$ with the
corresponding elements in $\bar{v}_{1}$ that encodes $D_{j}$ (note that
$v_{1,m+5},\dots,v_{1,m+4+|\bar{x}|}$ are interpretations for $\bar{x}$, and
$X_{i}\bar{x}^{\prime}[\bar{x}/(v_{1,m+5},\dots,v_{1,m+4+|\bar{x}|})]=X_{i}\bar{v}_{1}^{\prime}$).
We require that $X_{i}\bar{v}_{1}^{\prime}=X_{i}\bar{v}_{2}^{\prime}$, i.e.,
$\bar{v}_{1}^{\prime}=\bar{v}_{2}^{\prime}$. The following formula
$\alpha_{D_{j},X_{i}}(\bar{v}_{1},\bar{v}_{2})$ expresses that the atom
encoded by $\bar{v}_{2}$ occurs positively in clause $D_{j}$ encoded by
$\bar{v}_{1}$. For $i\in\\{1,\dots,k-1\\}$, define

$\alpha_{D_{j},X_{i}}(\bar{v}_{1},\bar{v}_{2})=\biggl{(}\varphi_{D_{j}}(\bar{v}_{1})\wedge\pi_{\mathrm{Var}_{i}}(\bar{v}_{2})\wedge\bigvee_{X_{i}\bar{x}^{\prime}\text{
occurs positively in
}D_{j}}\bar{v}_{1}^{\prime}=\bar{v}_{2}^{\prime}\biggr{)},$

and for $i\in\\{k,k+1\\}$, define

$\alpha_{D_{j},X_{i}}(\bar{v}_{1},\bar{v}_{2})=\biggl{(}\varphi_{D_{j}}(\bar{v}_{1})\wedge\pi_{\mathrm{Var}_{k}}(\bar{v}_{2})\wedge\mathrm{Var}_{i}(\bar{v}_{2})\wedge\bigvee_{X_{i}\bar{x}^{\prime}\text{
occurs positively in
}D_{j}}\bar{v}_{1}^{\prime}=\bar{v}_{2}^{\prime}\biggr{)}.$

Define $\pi_{\mathrm{Pos}}(\bar{v}_{1},\bar{v}_{2})$ to be the conjunction of
$v_{1,1}=v_{2,1}\wedge v_{1,3}=v_{2,3}$ and

$\bigvee\\{\alpha_{D_{j},X_{i}}(\bar{v}_{1},\bar{v}_{2})\ |\ X_{i}\text{ has a
positive occurrence in }D_{j}\\}.$

Similarly, we can define the formula
$\pi_{\mathrm{Neg}}^{\prime}(\bar{v}_{1},\bar{v}_{2})$ to express that the
atom encoded by $\bar{v}_{2}$ occurs negatively in clause $D_{j}$ $(1\leq
j\leq m)$ encoded by $\bar{v}_{1}$. For the clause $\forall\bar{y}\neg
X_{k+1}\bar{z}\bar{y}$, let $\bar{v}_{1}^{\prime\prime}$ and
$\bar{v}_{2}^{\prime\prime}$ be obtained by replacing $\bar{z}$ with the
corresponding elements in $\bar{v}_{1}$ that encodes the clause, and the
corresponding elements in $\bar{v}_{2}$ that encodes $X_{k+1}$, respectively.
Let

$\beta_{X_{k+1}}(\bar{v}_{1},\bar{v}_{2})=\left(\begin{array}[]{l}\pi_{\mathrm{Clause}}(\bar{v}_{1})\wedge(v_{1,1}=v_{1,4}\wedge\bigwedge_{5\leq
i\leq m+4}v_{1,3}=v_{1,i})\wedge\\\
\pi_{\mathrm{Var}_{k}}(\bar{v}_{2})\wedge\mathrm{Var}_{k+1}(\bar{v}_{2})\wedge
v_{1,1}=v_{2,1}\wedge
v_{1,3}=v_{2,3}\wedge\bar{v}_{1}^{\prime\prime}=\bar{v}_{2}^{\prime\prime}\end{array}\right).$

Define
$\pi_{\mathrm{Neg}}(\bar{v}_{1},\bar{v}_{2})=\pi_{\mathrm{Neg}}^{\prime}(\bar{v}_{1},\bar{v}_{2})\vee\beta_{X_{k+1}}(\bar{v}_{1},\bar{v}_{2})$.

Let $\Theta$ be the following formula

$\exists Z_{1}\forall Z_{2}\dots\exists Z_{k-1}\forall Z_{k}\exists
Y\forall\bar{v}_{1}\forall\bar{v}_{2}\left(\begin{array}[]{l}\exists\bar{z}Y(\bar{z})\wedge\Bigl{(}Y(\bar{v}_{1})\rightarrow\pi_{\mathrm{Clause}}(\bar{v}_{1})\Bigr{)}\wedge\\\
\bigwedge_{1\leq i\leq
k}\Bigl{(}Y(\bar{v}_{1})\wedge\pi_{\mathrm{Pos}}(\bar{v}_{1},\bar{v}_{2})\wedge\pi_{\mathrm{Var}_{i}}(\bar{v}_{2})\rightarrow
Z_{i}(\bar{v}_{2})\Bigr{)}\wedge\\\ \bigwedge_{1\leq i\leq
k}\Bigl{(}Y(\bar{v}_{1})\wedge\pi_{\mathrm{Neg}}(\bar{v}_{1},\bar{v}_{2})\wedge\pi_{\mathrm{Var}_{i}}(\bar{v}_{2})\rightarrow\neg
Z_{i}(\bar{v}_{2})\Bigr{)}\end{array}\right).$

The formula $\Theta$ says that there is a valuation for $X_{1}$, for any
valuation to $X_{2}$, …, there is a valuation to $X_{k-1}$, for any valuation
to $X_{k}$ and $X_{k+1}$, there is a nonempty set $Y$ of clauses, such that
all literals in the clauses are true under the valuation. $\Phi$ and $\Theta$
are equivalent on the structures with at least two elements. For any finite
structure, there is a quantifier-free formula that captures its isomorphism
type [EF95]. So on one-element structures, $\Phi$ is equivalent to $\forall
x\forall y(x=y\wedge\delta(x))$, where $\delta(x)$ is a disjunction of
isomorphism types of one-element structures satisfying $\Phi$. The formulas
$\Theta\vee\forall x\forall y(x=y\wedge\delta(x))$ and $\Phi$ are equivalent
on all finite structures. Since all formulas in $\Pi$ are quantifier-free,
$\Theta\vee\forall x\forall y(x=y\wedge\delta(x))$ can be converted to an
equivalent $\Sigma_{k+1}^{1}$-KROMr formula by elementary techniques.

The following proposition says that the data complexity of SO-KROMr is in the
polynomial hierarchy.

######  Proposition 10.

For each $k\geq 1$, if $k$ is odd, then the data complexity of
$\Pi^{1}_{k+1}\text{-}\mathrm{KROM}^{r}$ and
$\Pi^{1}_{k+2}\text{-}\mathrm{KROM}^{r}$ are in $\Pi^{p}_{k}$; if $k$ is even,
then the data complexity of $\Sigma^{1}_{k+1}\text{-}\mathrm{KROM}^{r}$ and
$\Sigma^{1}_{k+2}\text{-}\mathrm{KROM}^{r}$ are in $\Sigma^{p}_{k}$.

######  Proof 3.4.

From Corollary 2, we know that
$\Pi^{1}_{k+1}$-KROM${}^{r}\equiv\Pi^{1}_{k+2}$-KROMr if $k$ is odd, and
$\Sigma^{1}_{k+1}$-KROM${}^{r}\equiv\Sigma^{1}_{k+2}$-KROMr if $k$ is even. We
only prove that the data complexity of $\Pi^{1}_{k+1}$-KROMr is in
$\Pi^{p}_{k}$ ($k$ is odd), the proof for the other cases is similar.

Let
$\Phi=\forall\,\overline{\\!{X}}_{1}\exists\,\overline{\\!{X}}_{2}\dots\forall\,\overline{\\!{X}}_{k}\exists\,\overline{\\!{X}}_{k+1}\forall\bar{x}\varphi$
be a $\Pi^{1}_{k+1}$-KROMr formula ($k$ is odd). Given a structure
$\mathcal{A}$, we construct an alternating Turing machine that first assigns
the values of
$\,\overline{\\!{X}}_{1},\,\overline{\\!{X}}_{2},\dots,\,\overline{\\!{X}}_{k}$
alternately between universal and existential moves according to their
quantifier types. This step can be done in $\Pi^{p}_{k}$. The complexity of
deciding whether
$(\mathcal{A},\,\overline{\\!{X}}^{A}_{1},\,\overline{\\!{X}}^{A}_{2},\dots,\,\overline{\\!{X}}^{A}_{k})\models\exists\,\overline{\\!{X}}_{k+1}\forall\bar{x}\varphi$
is in NL, since all occurrences of $\exists\bar{z}X_{i}\bar{z}$ $(1\leq i\leq
k)$ in $\exists\,\overline{\\!{X}}_{k+1}\forall\bar{x}\varphi$ can be replaced
by their truth values, and the resulting formula is a $\Sigma^{1}_{1}$-KROMr
formula which can be evaluated in NL by Proposition 5. Therefore, the total
complexity of checking $\mathcal{A}\models\Phi$ is in $\Pi^{p}_{k}$.

Since $\Sigma^{1}_{k}$ captures $\Sigma^{p}_{k}$ and $\Pi^{1}_{k}$ captures
$\Pi^{p}_{k}$ for $k\geq 1$, combining Proposition 9 with Proposition 10 we
conclude the following corollary.

######  Corollary 11.

On all finite structures, for each $k\geq 1$, if $k$ is even, then
$\Sigma^{1}_{k+1}\text{-}\mathrm{KROM}^{r}\equiv\Sigma^{1}_{k}$, and if $k$ is
odd, then $\Pi^{1}_{k+1}\text{-}\mathrm{KROM}^{r}\equiv\Pi^{1}_{k}$.

######  Theorem 12.

On all finite structures, for each $k\geq 1$, if $k$ is even, then
$\Sigma^{1}_{k+1}\text{-}\mathrm{KROM}^{r}$ captures $\Sigma^{p}_{k}$, and if
$k$ is odd, then $\Pi^{1}_{k+1}\text{-}\mathrm{KROM}^{r}$ captures
$\Pi^{p}_{k}$.

##  4\. An extended version of second-order Krom logic

In this section, we define second-order extended Krom logic and study its
expressive power and data complexity. Second-order extended Krom logic over a
vocabulary $\tau$, denoted by SO-EKROM($\tau$), is the set of second-order
formulas of the form

$\forall X_{1}\exists Y_{1}\cdots\forall X_{k}\exists
Y_{k}\forall\bar{x}(C_{1}\wedge\cdots\wedge C_{n}),$

where $C_{i}$ $(1\leq i\leq n)$ are extended Krom clauses with respect to
$Y_{1},\dots,Y_{k}$, more precisely, each $C_{i}$ is a disjunction of the form

$\alpha_{1}\vee\cdots\vee\alpha_{l}\vee H_{1}\vee H_{2},$

where

  1. (1)

each $\alpha_{s}$ is either $Q\bar{y}$ or $\neg Q\bar{y}$, where
$Q\in\tau\cup\\{X_{1},\dots,X_{k}\\}$,

  2. (2)

each $H_{t}$ is either $Y_{i}\overline{z}$ or its negation $\neg
Y_{i}\overline{z}$, where $(1\leq i\leq k)$.

######  Proposition 13.

$\mathrm{SO\text{-}EKROM}$ is closed under substructures.

######  Proof 4.1.

All universal first-order formulas are closed under substructures. It is easy
to check that the formula obtained by quantifying a relation in a formula
which is closed under substructures still preserves this property.

######  Proposition 14.

The data complexity of $\mathrm{SO\text{-}EKROM}$ is in
$\mathrm{co\text{-}NP}$.

######  Proof 4.2.

Let $\Phi=\forall X_{1}\exists Y_{1}\dots\forall X_{k}\exists
Y_{k}\forall\bar{x}(C_{1}\wedge\cdots\wedge C_{n})$ be a SO-EKROM formula over
$\sigma$. For an arbitrary $\sigma$-structure $\mathcal{A}$, we replace the
first-order part $\forall\bar{x}(C_{1}\wedge\cdots\wedge C_{n})$ by
$\bigwedge_{\bar{a}\in A^{|\bar{x}|}}(C_{1}\wedge\cdots\wedge
C_{n})[\bar{x}/\bar{a}]$. We remove the clauses with a formula
$(\neg)R\bar{b}$ that is true in $\mathcal{A}$ and delete the formulas
$(\neg)R\bar{b}$ that are false in $\mathcal{A}$ in every clause, where $R$ is
a relation symbol in $\sigma$. Then we replace each second-order quantifier
$\forall X_{i}$ ($\exists Y_{i}$) in the prefix with a sequence $\forall
X_{i}\bar{d}_{1}\dots\forall X_{i}\bar{d}_{|A|^{arity(X_{i})}}$ ($\exists
Y_{i}\bar{d}_{1}\dots\exists Y_{i}\bar{d}_{|A|^{arity(X_{i})}}$) where each
$\bar{d}_{j}\in A^{arity(X_{i})}$. We treat the atoms $X_{i}\bar{d}_{j}$
($Y_{i}\bar{d}_{j}$) as propositional variables, the resulting formula $\psi$
is a QE-2CNF formula. It is clear that $\mathcal{A}\models\Phi$ iff $\psi$ is
true. It was proved that for any fixed number $m$, the evaluation problem for
the QE-2CNF formulas whose quantifier prefixes have $m$ alternations is in
$\mathrm{co\text{-}NP}$ [FKB90]. Hence, whether $\mathcal{A}\models\Phi$ holds
is decidable in $\mathrm{co\text{-}NP}$.

Since $\Pi^{1}_{1}$ captures co-NP, we can get the following corollary.

######  Corollary 15.

Every $\mathrm{SO\text{-}EKROM}$ formula is equivalent to a $\Pi^{1}_{1}$
formula on ordered finite structures.

######  Proposition 16.

$\Pi^{1}_{2}\text{-}\mathrm{KROM}^{r}\leq\Pi^{1}_{2}\text{-}\mathrm{EKROM}$ on
ordered finite structures.

######  Proof 4.3.

Let $\forall\,\overline{\\!{X}}\exists\mskip
1.5mu\overline{\mskip-1.5mu{Y}\mskip-1.5mu}\mskip 1.5mu\forall\bar{x}\varphi$
be a $\Pi^{1}_{2}$-KROMr formula. We see that $\exists\mskip
1.5mu\overline{\mskip-1.5mu{Y}\mskip-1.5mu}\mskip 1.5mu\forall\bar{x}\varphi$
is a $\Sigma^{1}_{1}$-KROMr formula. By Corollary 6, it is equivalent to a
$\Sigma^{1}_{1}\text{-KROM}$ formula on ordered finite structures. This
implies that $\forall\,\overline{\\!{X}}\exists\mskip
1.5mu\overline{\mskip-1.5mu{Y}\mskip-1.5mu}\mskip 1.5mu\forall\bar{x}\varphi$
is equivalent to a $\Pi^{1}_{2}\text{-EKROM}$ formula on ordered finite
structures.

Combining Proposition 9, Corollary 15 and Proposition 16 gives the following
corollary.

######  Corollary 17.

$\mathrm{SO\text{-}EKROM}\equiv\Pi^{1}_{2}\text{-}\mathrm{EKROM}\equiv\Pi^{1}_{1}$
on ordered finite structures.

######  Theorem 18.

Both $\mathrm{SO\text{-}EKROM}$ and $\Pi^{1}_{2}\text{-}\mathrm{EKROM}$ can
capture $\mathrm{co\text{-}NP}$ on ordered finite structures.

##  5\. Conclusion

In this paper, we introduce second-order revised Krom logic and study its
expressive power and data complexity. SO-KROMr is an extension of SO-KROM by
allowing $\exists\bar{z}R\bar{z}$ in the formula matrix, where $R$ is a
second-order variable. For SO-KROMr, we show that the innermost universal
second-order quantifiers can be removed. Hence,
$\Sigma^{1}_{k}$-KROM${}^{r}\equiv\Sigma^{1}_{k+1}$-KROMr for odd $k$, and
$\Pi^{1}_{k}$-KROM${}^{r}\equiv\Pi^{1}_{k+1}$-KROMr for even $k$. SO-KROM
collapses to its existential fragment. The same statement is unlikely to be
true for SO-KROMr. On ordered finite structures, we prove that
$\Sigma^{1}_{1}$-KROMr equals $\Sigma^{1}_{1}$-KROM, and captures NL. On all
finite structures, we show that $\Sigma^{1}_{k}\equiv\Sigma^{1}_{k+1}$-KROMr
for even $k$, and $\Pi^{1}_{k}\equiv\Pi^{1}_{k+1}$-KROMr for odd $k$. This
result gives an alternative logic for capturing the polynomial hierarchy,
which is the main contribution of the paper. We also study an extended version
of second-order Krom logic SO-EKROM. On ordered finite structures, SO-EKROM
collapses to $\Pi^{1}_{2}$-EKROM and equals $\Pi^{1}_{1}$. Therefore, both of
them can capture co-NP on ordered finite structures.

## References

  * [ABD09] Albert Atserias, Andrei Bulatov, and Anuj Dawar.  Affine systems of equations and counting infinitary logic.  Theoretical Computer Science, 410(18):1666–1683, 2009.
  * [AV89] Serge Abiteboul and Victor Vianu.  Fixpoint extensions of first-order logic and Datalog-like languages.  In Proceedings. Fourth Annual Symposium on Logic in Computer Science, pages 71–72. IEEE Computer Society, 1989.
  * [CK04] S. Cook and A. Kolokolova.  A second-order theory for NL.  In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004., pages 398–407, 2004.  doi:10.1109/LICS.2004.1319634.
  * [Daw08] Anuj Dawar.  On the descriptive complexity of linear algebra.  In International Workshop on Logic, Language, Information, and Computation, pages 17–25. Springer, 2008.
  * [DGHL09] Anuj Dawar, Martin Grohe, Bjarki Holm, and Bastian Laubner.  Logics with rank operators.  In Logic In Computer Science, 2009. LICS’09. 24th Annual IEEE Symposium on, pages 113–122. IEEE, 2009.
  * [DGP19] Anuj Dawar, Erich Grädel, and Wied Pakusa.  Approximations of isomorphism and logics with linear-algebraic operators.  In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019, Patras, Greece, volume 132 of LIPIcs, pages 112:1–112:14, 2019.
  * [EF95] Heinz-Dieter Ebbinghaus and Jörg Flum.  Finite model theory.  Springer-Verlag Berlin Heidelberg, 1995.
  * [Fag74] R. Fagin.  Generalized first-order spectra and polynomial-time recognizable sets.  SIAM-AMS Proceedings, 7:43–73, 1974.
  * [FKB90] Andreas Flögel, Marek Karpinski, and Hans Kleine Büning.  Subclasses of quantified boolean formulas.  In Proceedings of the 4th Workshop on Computer Science Logic, CSL 1990, page 145–155, Berlin, Heidelberg, 1990. Springer-Verlag.
  * [FZ12] Shiguang Feng and Xishun Zhao.  The complexity and expressive power of second-order extended logic.  Studies in Logic, 5(1):11–34, 2012.
  * [FZ13] Shiguang Feng and Xishun Zhao.  Complexity and expressive power of second-order extended Horn logic.  Mathematical Logic Quarterly, 59(1-2):4–11, 2013.
  * [GO92] Erich Grädel and Martin Otto.  Inductive definability with counting on finite structures.  In Selected Papers from the Workshop on Computer Science Logic, CSL ’92, page 231–247, Berlin, Heidelberg, 1992. Springer-Verlag.
  * [Grä91] Erich Grädel.  The expressive power of second order Horn logic.  In Annual Symposium on Theoretical Aspects of Computer Science, pages 466–477. Springer, 1991.
  * [Grä92] Erich Grädel.  Capturing complexity classes by fragments of second-order logic.  Theoretical Computer Science, 101(1):35–57, 1992.
  * [Imm82] Neil Immerman.  Relational queries computable in polynomial time.  In fourteenth annual ACM symposium on Theory of computing, pages 147–152. ACM, 1982.
  * [Imm87] Neil Immerman.  Languages that capture complexity classes.  SIAM Journal on Computing, 16(4):760–778, 1987.
  * [Imm98] Neil Immerman.  Descriptive Complexity.  Springer Verlag, 1998.
  * [Ott96] Martin Otto.  The expressive power of fixed-point logic with counting.  Journal of Symbolic Logic, pages 147–176, 1996.
  * [Sto76] Larry J. Stockmeyer.  The polynomial-time hierarchy.  Theoretical Computer Science, 3(1):1–22, 1976.
  * [Var82] Moshe Y Vardi.  The complexity of relational query languages.  In fourteenth annual ACM symposium on Theory of computing, pages 137–146. ACM, 1982.