The Complexity and Expressive Power of Second-Order Extended Logic

Descriptive complexity is a bridge between complexity theory and mathematical logic. It uses logic systems to measure the resources that are necessary for some complexity classes. The first capture result is Fagin’s theorem. In 1974, Fagin showed that existential second-order logic($\exists$SO) captures NP on all finite structures. This is a seminal work that has been followed by many studies in the characterization of other complexity classes by means of logical systems, the research of NP-complete approximation problems from a descriptive point of view, and so on. Through the effort of many researchers in this area, almost every important complexity classes have their corresponding capture logic systems. First-order logic (FO) which is a very powerful logic in classic model theory is too weak when only consider finite structures. By augmenting some recursion operators, researchers got many powerful logic. FO(IFP), FO(PFP), FO(DTC) and FO(TC) are the logic that equip first-order logic with inflationary fixpoint operator, partial fixpoint operator, deterministic transitive closure operator and transitive closure operator, respectively. Immerman and Vardi both showed that FO(IFP) captures PTIME on ordered structures in 1986 and 1982, respectively. Abiteboul and Vainu showed that FO(PFP) captures PSPACE on ordered structures in 1983. Immerman showed that FO(DTC) and FO(TC) capture L and NL on ordered structures, respectively, in 1987. In[4], Grädel introduced SO-HORN logic which is a fragment of second-order logic and showed that SO-HORN captures PTIME on ordered structures. Whereas all these results are obtained on ordered structures, a very important open problem in descriptive complexity is that whether there is an effective logic captures PTIME on all structures. It turns out that if there is no such a logic, then $P\neq NP$. Due to the definition of SO-HORN, on all structures, it is closed under substructures and can not express some first-order definable properties. Grädel introduced another version of this logic in [6] which is called SO-HORN^∗ in this paper. SO-HORN^∗ allows first-order formula in it, but we show that it still is not expressive enough to capture PTIME on all structures. In[21], we defined SO-HORN^r logic which is an revised version of SO-HORN and showed that it captures PTIME on ordered structures. We are interested in finding that whether this logic can be a candidate to capture PTIME on all finite structures. To study the expressive powers of these logic on all finite structures, we introduce the notions of DATALOG^∗ program and DATALOG^r program and their stratified versions (S-DATALOG^∗, S-DATALOG^r, respectively). In this paper, we show that SO-HORN^r has the same expressive power as FO(LFP) which is a very powerful logic. We also study the expressive power of SO-EHORN^r and prove that SO-EHORN^r captures co-NP on all finite structures. This logic is an extended version of SO-HORN and has been shown that it can capture co-NP on ordered structures.

This paper is organized as follows: In section 2, we set up notations and terminologies. In section 3, we study the expressive powers of SO-HORN^∗, SO-HORN^r and SO-HORN^∗r on all finite structures. We use DATALOG and S-DATALOG program as intermediate logic, and introduce the notions of DATALOG^∗ program, DATALOG^r program and their stratified versions. We show that SO-HORN^r, SO-HORN^∗r, FO(LFP) coincide with each other and SO-HORN^∗ is a proper sublogic of SO-HORN^r. In section 4, we use the normal forms of $\Sigma_{1}^{1}$ formulas to show that SO-EHORN^r captures co-NP on all finite structures. We prove this result in two versions. Section 5 is the conclusion of this paper.

We assume the reader has already some familiarity with mathematical logic and complexity theory. Nonetheless, we give a brief description of some basic definitions.

A vocabulary is a finite set of relation symbols $P,Q,R,\cdots$ and constant symbols $\mathbf{c},\mathbf{d},\cdots$. Each relation symbol is equipped with a natural number $r\geq 1$, its arity. We use lower-case Greek letters $\tau,\sigma,\cdots$ to denote a vocabulary. Given a vocabulary $\tau=\{P_{1},P_{2},\cdots,P_{n},\mathbf{c}_{1},\mathbf{c}_{2},\cdots,\mathbf{c}_{m}\}$, a $\tau$-structure $\mathcal{A}$ is a tuple

where $A$ is the domain of $\mathcal{A}$, for each relation symbol $P_{i}$ of arity $r_{i}\,(1\leq i\leq n)$, $P_{i}^{A}\subseteq A^{r_{i}}$ and for each constant symbol $\mathbf{c}_{j}\,(1\leq j\leq m)$, $\mathbf{c}_{j}^{A}\in A$. From now on, we use calligraphic letters $\mathcal{A},\mathcal{B},\cdots$ and capital letters $A,B,\dots$ to denote structures and the corresponding domains, respectively. We use $|A|$ to denote the cardinality of set $A$ and $\bar{a}$ to denote a sequence $a_{1},a_{2},\cdots,a_{n}$ or a tuple $(a_{1},a_{2},\cdots,a_{n})$ of elements (variables). A structure $\mathcal{A}$ is finite if its domain $A$ is a finite set. Without otherwise specified, we restrict ourself to finite structures in this paper. Let $STRUC(\tau)$ denote the set of all finite $\tau$-structures, and if $\mathcal{L}$ is a logic, then $\mathcal{L}(\tau)$ denotes the set of all formulas of $\mathcal{L}$ over the vocabulary $\tau$. Given a formula $\phi\in\mathcal{L}(\tau)$, define

Let $\mathcal{L}_{1}$ and $\mathcal{L}_{2}$ be two logic, we use $\mathcal{L}_{1}\subseteq\mathcal{L}_{2}$ to denote the expressive power of $\mathcal{L}_{2}$ is no less than that of $\mathcal{L}_{1}$, i.e. for any vocabulary $\tau$ and any $\phi\in\mathcal{L}_{1}(\tau)$, there exists $\psi\in\mathcal{L}_{2}(\tau)$ such that $Mod(\phi)=Mod(\psi)$. $\mathcal{L}_{1}\subset\mathcal{L}_{2}$ denotes that $\mathcal{L}_{2}$ is strictly more expressive than $\mathcal{L}_{1}$, and $\mathcal{L}_{1}\equiv\mathcal{L}_{2}$ denotes that $\mathcal{L}_{1}$ has the same expressive power as $\mathcal{L}_{2}$.

Define $\tau_{<}=\tau\cup\{<,succ,\mathbf{min},\mathbf{max}\}$, where $\tau$ is a vocabulary. A $\tau_{<}$-structure $\mathcal{A}$ is ordered if the reduct $\mathcal{A}\mid\{<,succ,\mathbf{min},\mathbf{max}\}$ is an ordering (that is, $<$, $succ$, $\mathbf{min}$ and $\mathbf{max}$ are interpreted by the ordering relation, successor relation, the least and the last element of the ordering, respectively.) Let $STRUC_{<}(\tau)$ denote the set of all ordered structures over $\tau_{<}$. Given a formula $\phi\in\mathcal{L}(\tau_{<})$, define

Let $\mathcal{L}$ be a logic and $\mathcal{C}$ be a complexity class, we say logic $\mathcal{L}$ captures complexity class $\mathcal{C}$ if the following two conditions are satisfied:

1)

The data complexity of $\mathcal{L}$ is in $\mathcal{C}$.

• •

  For any vocabulary $\tau$ and any closed formula $\phi\in\mathcal{L}(\tau)$, the membership problem of $Mod(\phi)$ is in $\mathcal{C}$.

2)

$\mathcal{C}$ is expressible in $\mathcal{L}$.

• •

  For any vocabulary $\tau$ and any set $K\subseteq STRUC(\tau)$, if the membership problem of $K$ is in $\mathcal{C}$, then $\exists\phi\in\mathcal{L}(\tau)$ such that $K=Mod(\phi)$.

We say $\mathcal{L}$ captures $\mathcal{C}$ on ordered structures if we only consider ordered structures and it satisfies:

1)

For any vocabulary $\tau$ and any closed formula $\phi\in\mathcal{L}(\tau_{<})$, the membership problem of $Mod_{<}(\phi)$ is in $\mathcal{C}$.

2)

For any vocabulary $\tau$ and any set $K\subseteq STRUC_{<}(\tau)$, if the membership problem of $K$ is in $\mathcal{C}$, then $\exists\phi\in\mathcal{L}(\tau_{<})$ such that $K=Mod_{<}(\phi)$.

We recall some notions and results of quantified Boolean formulas (QBF). A QBF formula has the form:

where $Q_{i}\in\{\forall,\exists\}$ and $\varphi$ is a propositional CNF formula over Boolean variables. A literal $x_{i}$ or $\neg x_{i}$ is called universal (resp. existential) if $Q_{i}$ is $\forall$ (resp. $\exists$). If every clause in $\varphi$ contains at most one positive literal (resp. positive existential literal) then $\Phi$ is called a quantified Horn formula (QHORN) (resp. quantified extended Horn formula (QEHORN)). The evaluation problem for QBF is PSPACE-complete [9], for QHORN is in PTIME, whereas it remains PSPACE-complete for QEHORN. However, for each fixed $k\geq 1$, the evaluation problem for QEHORN formulas with prefix type $\forall\overline{x}_{1}\exists\overline{y}_{1}\cdots\forall\overline{x}_{k}\exists\overline{y}_{k}$ (here $\overline{x}_{i},\overline{y}_{i}$ are sequences of Boolean variables) is co-NP complete[1, 2].

On ordered structures, Grädel[4, 6] showed that SO-HORN and SO-HORN^∗ capture PTIME and we[21] showed that SO-HORN^∗r captures PTIME. These four logic coincide with each other. On all structures, it turns out that SO-HORN is strictly less expressive than FO(LFP) which is a very powerful logic. It is not hard to see that the following holds from the definition above:

An important open problem in descriptive complexity is that whether there is an effective logic captures PTIME on all structures. We are interesting in finding the expressive powers of these Horn logic on all structures. At first, we give a lemma that is very useful. Let $\phi$ be a logic formula, we use $\phi[\alpha/\beta]$ to denote the formula obtained by replacing the formula $\alpha$ by $\beta$ in $\phi$.

It turns out that SO-HORN collapses to its existential fragment ((SO$\exists$)-HORN, i.e. the formulas where all the second-order quantifiers are existential[4]). In fact, many second-order formulas equal to the formulas that only have existential second-order prefix. We extend this result to a more general form in the following proposition.

From now on, unless explicitly stated, we will restrict ourselves to the existential fragments of these logic defined above in the rest of this paper. To compare the expressive power of the four logic on all structures, we use DATALOG and S-DATALOG program as intermediate logic, and introduce the notion of DATALOG^r program. For the detailed definition and semantics of DATALOG program and S-DATALOG program we refer the reader to [8].

$\alpha_{1},\cdots,\alpha_{l}$ constitute the body of the rule, $\beta$ is the head of the rule. Every relation symbols in the head of some rule of $\Pi$ are intentional, all the other symbols are extensional. We use $(\tau,\Pi)_{int}$ and $(\tau,\Pi)_{ext}$ to denote the set of intentional and extensional symbols(constant symbols are extensional symbols), respectively. We allow zero-ary relation symbols here to be able to compare the expressive power of DATALOG with other logic. A zero-ary relation has the Boolean value TRUE or FALSE. Let $Q$ be a zero-ary relation symbol and $\mathcal{A}$ be a structure, the interpretation of $Q$ in $\mathcal{A}$ is: “$Q^{A}=\emptyset$” means “$Q^{A}=FALSE$”, “$Q^{A}=\{\emptyset\}$” means “$Q^{A}=TRUE$”.

Instead of giving a detailed definition of the semantics of DATALOG programs, we present it briefly using an example. Given a DATALOG program $\Pi$ and a $(\tau,\Pi)_{ext}$-structure, we can apply all the rules of $\Pi$ simultaneously to generate consecutive stages of the intentional symbols. Consider the above example, let $R_{(0)}=\emptyset$, $Q_{(0)}=\emptyset$ and $\mathcal{A}$ be a $(\tau,\Pi)_{ext}$-structure. Suppose $R_{(i)}$ and $Q_{(i)}$ are known, $R_{(i+1)}$ and $Q_{(i+1)}$ can be evaluated by

where $Q_{(i+1)}=\{\emptyset\}$ iff $\mathcal{A}\models R_{(i)}\mathbf{st}$. Because $R$ occurs only positively in the body of each rules, we can reach a fixed-point in polynomial many steps with respect to $|A|$. Let $R_{(\infty)}=\underset{n\geq 0}{\bigcup}R_{(n)}$ denote the fixed-point. Then $\mathcal{A}$ gives rise to a $\tau$-structure

A DATALOG formula has the form $(\Pi,P)\bar{t}$ where $P$ is an $r$-ary intentional relation symbol and $\bar{t}=t_{1},\cdots,t_{r}$ are variables that don’t occur in $\Pi$. Given a $(\tau,\Pi)_{ext}$-structure $\mathcal{A}$ and $\bar{a}=a_{1},\cdots,a_{r}\in A$

If $P$ is a zero-ary relation symbol, then

In the above example, given $a,b\in A$,

For a DATALOG ( DATALOG^∗, DATALOG^r, DATALOG^∗r, respectively ) program $\Pi$, if there is a zero-ary relation symbol occurring in the body of some rules, e.g. $Q$, we replace every occurrences of $Q$ by $Q^{\prime}x$, where $Q^{\prime}$ is a new relation symbol and $x$ is a new variable that do not occur in $\Pi$, and then add the rule $Q\leftarrow Q^{\prime}x$ in $\Pi$. Let $\Pi^{\prime}$ denote the resulting DATALOG ( DATALOG^∗, DATALOG^r, DATALOG^∗r, respectively ) program. It is easily check that the fixed-points of all common intentional relations of $\Pi$ and $\Pi^{\prime}$ coincide on all structures. So for technical reason, unless stated explicitly, we restrict that the zero-ary relation symbols only occur in the head of a rule.

It turns out that many first-order definable properties can not be defined by DATALOG formulas. DATALOG^∗ and DATALOG^∗r programs which are equipped with first-order formulas are more expressive than DATALOG programs. In the following we show that DATALOG^r formulas is enough to express all first-order definable properties. We say a DATALOG ( DATALOG^∗, DATALOG^r, DATALOG^∗r, respectively) formula $(\Pi,P)\bar{t}$ is bounded if there exists a fixed number $k\geq 0$ such that $P_{(k)}=P_{(\infty)}$ for all structures.

A DATALOG program $\Pi$ is positive if no atomic occurs negatively in any rule of $\Pi$. M. Ajtai and Y. Gurevich[12] showed that a positive DATALOG formula is bounded if and only if it is equivalent to a (existential positive) first-order formula. For a DATALOG formula, if it is bounded then it equals to a first-order formula, but the converse is false. They find a DATALOG formula which is equivalent to a first-order formula but not bounded. We show that this statement is true for DATALOG^r formulas.

Corollary 2 shows that DATALOG^∗ programs is a sublogic of DATALOG^r programs. In fact, it is proper. Before proving this result, we review stratified DATALOG program ( by short: S-DATALOG program ) which is more powerful than DATALOG program.

Given a S-DATALOG program $\Sigma=(\Pi_{0},\Pi_{1},\cdots,\Pi_{n})$ and a $(\tau_{0},\Pi_{0})_{ext}$-structure $\mathcal{A}$, we set

A S-DATALOG formula has the form $(\Sigma,P)\bar{t}$ where $P$ is an $r$-ary intentional relation symbol of one of the constitutes $\Pi_{i}$ and $\bar{t}=t_{1},\cdots,t_{r}$ are variables that do not occur in $\Sigma$.