Expressiveness of Logic Programs under General Stable Model Semantics %\\(full version)
Heng Zhang
Yan Zhang
Artificial Intelligence Research Group
School of Computing
Engineering and Mathematics
University of Western Sydney
Australia
\begin{quote The stable model semantics had been recently generalized to non-Herbrand structures by several works, which provides a unified framework and solid logical foundations for answer set programming. This paper focuses on the expressiveness of normal and disjunctive programs under the general stable model semantics. A translation from disjunctive programs to normal programs is proposed for infinite structures. Over finite structures, some disjunctive programs are proved to be intranslatable to normal programs if the arities of auxiliary predicates and functions are bounded in a certain way. The equivalence of the expressiveness of normal programs and disjunctive programs over arbitrary structures is also shown to coincide with that over finite structures, and coincide with whether NP is closed under complement. Moreover, to capture the exact expressiveness, some intertranslatability results between logic program classes and fragments of second-order logic are obtained. \end{quote
lp_exp.tex
%File: formatting-instruction.tex
\documentclass[letterpaper]{article}
%\usepackage{aaai}
\usepackage{times}
\usepackage{helvet}
\usepackage{courier}

\usepackage{mathrsfs}
\usepackage{dsfont}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{amssymb}

%\usepackage{hyperref}

% THEOREM Environments ------------------------------------
\newcounter{theorem}
\newcounter{definition}
\newcounter{remark}

\newtheorem{thm}{Theorem}
\newtheorem{cor}{Corollary}
\newtheorem{lem}{Lemma}
\newtheorem{prop}{Proposition}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\theoremstyle{remark}
\newtheorem{rem}{Remark}
\theoremstyle{definition}
\newtheorem{exm}{Example}


\frenchspacing
\setlength{\pdfpagewidth}{8.5in}
\setlength{\pdfpageheight}{11in}
\pdfinfo{
/Title (Expressiveness of Logic Programs under General Stable Model Semantics)
/Author (Heng Zhang, Yan Zhang)}
\setcounter{secnumdepth}{0}
 \begin{document}
% The file aaai.sty is the style file for AAAI Press
% proceedings, working notes, and technical reports.
%
\title{
Expressiveness of Logic Programs under General Stable Model Semantics
%\\(full version)
}
\author{Heng Zhang \and Yan Zhang\\
Artificial Intelligence Research Group\\
School of Computing, Engineering and Mathematics\\ University of Western Sydney, Australia
}
\maketitle
\begin{abstract}
\begin{quote}
The stable model semantics had been recently generalized to non-Herbrand structures by several works, which provides a unified framework and solid logical foundations for answer set programming. This paper focuses on the expressiveness of normal and disjunctive programs under the general stable model semantics. A translation from disjunctive programs to normal programs is proposed for infinite structures. Over finite structures, some disjunctive programs are proved to be intranslatable to normal programs if the arities of auxiliary predicates and functions are bounded in a certain way. The equivalence of the expressiveness of normal programs and disjunctive programs over arbitrary structures is also shown to coincide with that over finite structures, and coincide with whether NP is closed under complement. Moreover, to capture the exact expressiveness, some intertranslatability results between logic program classes and fragments of second-order logic are obtained.
\end{quote}
\end{abstract}

\section{Introduction}

Logic programming with default negation is an elegant and efficient formalism for knowledge representation, which incorporates the abilities of classical logic, inductive definition and commonsense reasoning. Nowadays, the most popular semantics for this formalism is the stable model semantics proposed by~\cite{GL:88}. Logic programming based on this semantics, which is known as answer-set programming, has then emerged as a flourishing paradigm for declarative programming in the last fifteen years.


The original stable model semantics focuses only on Herbrand structures in which the unique name assumption is made. For a certain class of applications, this assumption will simplify the representation. However, there are many applications where the knowledge can be more naturally represented over non-Herbrand structures, including arithmetical structures and other metafinite structures. To overcome this limit, the general stable model semantics, which generalizes the original semantics to arbitrary structures, was then proposed by~\cite{FLL:11} via second-order logic, by~\cite{LZ:11} via circumscription, and by~\cite{PV:05} via G\"{o}del's 3-valued logic,
which provides us a unified framework for answer set programming, armed with powerful tools from classical logic.

%The general stable semantics turns out to be an elegant and unified semantical framework for answer set programming. In recent years, it was proved that a wide range of knowledge presentation languages, including  can be naturally translated into logic programs under this semantics.
%
%Logic programs under the general stable semantics turn out to be a very general language for knowledge representation. A .
%
%
%Identifying the expressiveness of a language is one of the central topics in the community of Knowledge Representation and Reasoning.
%
% Disjunctive logic programs extend this language by introducing epistemic disjunction to the rule head, motivated to represent more knowledge, in particular, indefinite knowledge. The most popular semantics for them is the stable model semantics, which was originally proposed by~\cite{GL:88}. Logic programming based on it is known as answer set programming, a flourishing paradigm of declarative programming emerged recently.

The main goal of this work is to identify the expressiveness of logic programs, which is one of the central topics in knowledge representation and reasoning. We will focus on two important classes of logic programs -- normal programs and disjunctive programs. Over Herbrand structures, the expressiveness of logic programs under the query equivalence has been thoroughly studied in the last three decades. An excellent survey for these works can be found in~\cite{DEGV:01}. Our task is quite different. On the one hand, we will work on the general stable model semantics so that non-Herbrand structures will be considered. On the other hand, instead of considering query equivalence, the expressiveness in our work will be based on model equivalence. This setting is important since answer set solvers are usually used to generate models. The model equivalence implies the query equivalence, but the converse is in general not true.

We also hope this work contributing to the effective implementation of answer set solvers. Translating logic programs into classical logics is a usual approach to implement answer set solvers, e.g.,~\cite{LZ:04,LM:04}. In this work, we are interested in translating normal programs to first-order sentences so that the state-of-the-art SMT solvers can be used for answer set solving. As the arity of auxiliary symbol is the most important factor to introduce nondeterminism~\cite{Imme:99}, we will try to find translations with small arities of auxiliary symbols.  %As disjunctions and auxiliary predicates are two important reasons introducing nondeterminism, these will be important for optimization.


%  Disjunctions and auxiliary predicates are two important formalism to introduce nondeterminism   %Normally, a programming language is more flexible to encode problems, it will more difficult to be efficiently implemented.
%In declarative programming,
%Normally, a programming language should be flexible enough so that various problems can be naturally encoded; however, %from the solver developer's view point, a complex language is very difficult to be implemented.
%To reconcile the contradiction, it is important to know the (in)translatability between subclasses of this language. We will focus on the (in)translatability of logic programs with variables, which is different that for propositional programs.

%In this work, we will consider: in which case the disjunction can be eliminated,  answer set programming, disjunctions and auxiliary predicates are two important resources to provide the nondeterminism.

%Identifying the expressive power of languages is one of the central topics in the area of knowledge representation and reasoning. In this paper we try to compare the expressive power of these two kinds of logic programs under the stable model semantics. The expressive power of logic programs as a database query language has been thoroughly studied in last three decades. For a survey, please refer to~\cite{DEGV:01}. However, except for a few work, the results for normal and disjunctive logic programs are limited to Herbrand structures. As encoding knowledge in Herbrand domains is unnatural and inflexible in many cases, our work will focus on infinite structures, finite structures and arbitrary structures. The semantics employed here is the general stable model semantics, which was developed by~\cite{FLL:11,LZ:11} via a second-order translation, and provides us a unified framework for answer set programming.

%In this paper we try to compare the expressive power of two important languages for knowledge representation and logic programming: disjunctive and normal logic programs. The most popular semantics for them are the stable model semantics, which was originally proposed by~\cite{GL:88}, and had been recently generalized to non-Herbrand structures by~\cite{FLL:11,LZ:11} via a second-order transformation.
%
%
%, and had been recently generalized to non-Herbrand structures by~\cite{FLL:11,LZ:11} via a second-order transformation.
%
%We focus on the stable model semantics, which was originally proposed by~\cite{GL:88}, and lay a foundation for    answer-set programming. This semantics was recently ... which provides us a unified ... and a solid logical foundation.

% Answer-set programming

%as a fragment of circumscription
%as a manageable fragment of second-order logic.

%A bunch of solvers, including DLV~\cite{}, claspD~\cite{}, and CModel~\cite{}

%There is a lot of work on

%Logic programming, a brief history review, Prolog => datalog => answer-set programming => disjunctive logic programming. General stable models.
%
%Expressive power: previous work on Herbrand structures.

Our contribution in this paper is fourfold. Firstly, we show that, over infinite structures, every disjunctive program can be equivalently translated to a normal one. Secondly, we prove that, if finite structures are focused, for each integer $n$ greater than $1$ there is a disjunctive program with intensional predicates of arities less than $n$ that cannot be equivalently translated to any normal program with auxiliary predicates of arities less than $2n$.  Thirdly, we show that disjunctive and normal programs are of the same expressiveness over arbitrary structures if and only if they are of the same expressiveness over finite structures, if and only if the complexity class NP is closed under complement. Lastly, to understand the exact expressiveness of logic programs, we also prove that the intertranslatability holds between some classes of logic programs and some fragments of second-order logic.

\section{Preliminaries}

{\em Vocabularies} are assumed to be sets of predicate constants
and function constants.
Logical symbols are as usual, including a countable set of
predicate variables and a countable set of function variables. Every constant or variable is equipped with a natural number, its {\em arity}. Nullary function constants and variables are called {\em individual constants} and {\em variables} respectively. Nullary predicate constants are called {\em propositions}. Sometimes, we do not distinguish between constants and variables, and simply call them {\em predicates} or {\em functions}
%Predicate (respectively, function) constants and variables are simply called {\em predicates} (respectively, {\em functions})
if no confusion occurs.
Atoms, formulas, sentences and theories of a vocabulary $\upsilon$ (or shortly,
$\upsilon$-atoms, $\upsilon$-formulas, $\upsilon$-sentences and $\upsilon$-theories) are built
from $\upsilon$, equality, variables, connectives and quantifiers in a standard way. Every {\em positive clause} of $\upsilon$ is a finite disjunction of $\upsilon$-atoms.
%The only thing which
%may be special is that we treat $\neg\varphi$ as a shorthand of
%$\varphi\rightarrow\bot$, and $\varphi\leftrightarrow\psi$ as the
%conjunction of $\varphi\rightarrow\psi$ and
%$\psi\rightarrow\varphi$.
Given a sentence $\varphi$ and a theory $\Sigma$, let $\upsilon(\varphi)$ and $\upsilon(\Sigma)$ denote the sets of constants occurring in $\varphi$ and $\Sigma$ respectively.

Assuming $\mathsf{Q}$ to be $\forall$ or $\exists$, let $\mathsf{Q}\tau$ and $\mathsf{Q}\bar{x}$ denote the quantifier blocks $\mathsf{Q}X_1\cdots\mathsf{Q}X_n$ and $\mathsf{Q}x_1\cdots\mathsf{Q}x_m$ respectively if $\tau$ is the finite set $\{X_1,\dots,X_n\}$, $\bar{x}=x_1\cdots x_m$, $X_i$ and $x_i$ are predicate/function and individual variables respectively.
%A first-order (second-order) formula of the form $\forall\bar{x}\vartheta$ ($\forall\tau\vartheta$) is {\em universal} if no first-order (second-order) quantifiers occurs in $\vartheta$.
Let $\Sigma${\small$^{1\textsc{f}}_{n,k}$} be the class of sentences of form
$
\mathsf{Q}_1\tau_1\cdots\mathsf{Q}_n\tau_n\varphi
$,
where $\mathsf{Q}_i$ is $\exists$ if $i$ is odd, otherwise it is $\forall$; $\tau_i$ is a finite set of variables of arities $\le k$; and no second-order quantifier %(i.e., quantifiers with predicate variable, or function variable of arity $>0$)
appears in $\varphi$. Let $\Sigma${\small$^{1}_{n,k}$} denote the class defined as the same as $\Sigma${\small$^{1\textsc{f}}_{n,k}$} except no function variable allowed in any $\tau_i$. Let $\Sigma${\small$^{1\textsc{f}}_{n}$} (respectively, $\Sigma${\small$^{1}_{n}$}) be the union of $\Sigma${\small$^{1\textsc{f}}_{n,k}$} (respectively, $\Sigma${\small$^{1}_{n,k}$}) for all $k\ge 0$. Given a class $\Sigma$ defined as above, let $\Sigma[\forall^{\ast}\exists^{\ast}]$ (respectively, $\Sigma[\forall^{\ast}]$) be the class of sentences in $\Sigma$ with first-order part of form $\forall\bar{x}\exists\bar{y}\vartheta$ (respectively, $\forall\bar{x}\vartheta$), where $\bar{x}$ and $\bar{y}$ are tuples of individual variables, and $\vartheta$ quantifier-free.

%
%A first-order formula $\varphi$ is said to be in the form $\mathsf{Q}_1^{c_1}\mathsf{Q}_2^{c_2}\cdots\mathsf{Q}_n^{c_n}$ (called it a {\em quantifier pattern}, where $\mathsf{Q}_i$ is $\exists$ or $\forall$, and $c_i$ is ``$\ast$" or a natural number) if it is in prenex normal form and the quantifier part is of form $\mathsf{Q}_1\bar{x}_1\cdots Q_n\bar{x}_n$ such that $\bar{x}_i$ is an individual-variable tuple of length less than $c_i$ (in particular, the length can be any natural number if $c_i=\ast$). Given a class $\Sigma$ of sentences and a quantifier pattern $\mathsf{Q}_1^{c_1}\cdots\mathsf{Q}_n^{c_n}$, let $\Sigma[\mathsf{Q}_1^{c_1}\cdots\mathsf{Q}_n^{c_n}]$ be the class of sentences whose first-order part is in form $\mathsf{Q}_1^{c_1}\cdots\mathsf{Q}_n^{c_n}$.
%
%prenex normal form with second-order quantifiers preceding all first-order quantifiers and whose second-order quantifier

%Let $\Sigma^1_{n,k}$ denote the set of second-order
%sentences of the form
%$Q_1\tau_1\cdots Q_n\tau_n\varphi$, where $Q_i(1\leq i\leq n)$ is $\exists$ if $i$ is odd, otherwise $Q_i$ is $\forall$;  $\varphi$ is first-order; and every predicate or function variable is of arity $\leq k$. Let $\Sigma^1_n$ be the union of $\Sigma^1_{n,k}$ for all $k\geq 0$. In particular, let $\mathrm{ESO}$ be the set of {\em existential second-order sentences}, i.e., sentences in $\Sigma^1_1$. A {\em quantifier prefix} is a string on the alphabet $\{\forall^{\ast},\exists^{\ast},\forall^1,\exists^1,\forall^2,\exists^2,\dots\}$. $\Sigma^1_n[\forall^k\exists^{\ast}]$

Every {\em structure} $\mathds{A}$ of $\upsilon$ (or
shortly, {\em $\upsilon$-structure} $\mathds{A}$) is accompanied by
a nonempty set $A$, the {\em domain} of $\mathds{A}$, and
interprets each $n$-ary predicate constant $P$ in $\upsilon$ as an
$n$-ary relation $P^{\mathds{A}}$ on $A$, and interprets each
$n$-ary function constant $f$ in $\upsilon$ as an $n$-ary function
$f^{\mathds{A}}$ on $A$. A structure is {\em finite} if its domain is finite; otherwise it is {\em infinite}. Let $\mathsf{FIN}$ denote the class of finite structures, and let $\mathsf{INF}$ denote the class of infinite structures.
%Given two $\upsilon$-structures $\mathds{A},\mathds{B}$ with the same domain and a set $\tau$ of predicates, we write $\mathds{A}\preccurlyeq_{\tau}\mathds{B}$ if the interpretation of each predicate of $\tau$ in $\mathds{A}$ is a subset of that in $\mathds{B}$, and interpretations of other predicates and functions in $\mathds{A}$ are same as that in $\mathds{B}$; we write $\mathds{A}\prec_{\tau}\mathds{B}$ if $\mathds{A}\preccurlyeq_{\tau}\mathds{B}$ holds but  $\mathds{B}\preccurlyeq_{\tau}\mathds{A}$ does not.
A {\em restriction} of
a structure $\mathds{A}$ to a vocabulary $\sigma$ is the structure obtained
from $\mathds{A}$ by discarding all interpretations for constants
not in $\sigma$. Given a vocabulary $\upsilon\supset\sigma$ and a
$\sigma$-structure $\mathds{B}$,
every {\em $\upsilon$-expansion} of $\mathds{B}$ is a structure $\mathds{A}$ of $\upsilon$ such that
$\mathds{B}$ is a restriction of $\mathds{A}$ to $\sigma$. Given a structure $\mathds{A}$ and a set $\tau$ of predicates,
let $\textsc{Ins}(\mathds{A},\tau)$ be the set of {\em ground atoms} $P(\bar{a})$ for all $\bar{a}\in P^{\mathds{A}}$ and all $P$ in $\tau$.

Every {\em assignment} in a structure
$\mathds{A}$ is a function that maps each individual
variable to an element of $A$ and maps each predicate (respectively, function)
variable to a relation (respectively, function) on $A$ of the same arity. Given a formula $\varphi$
and an assignment $\alpha$ in $\mathds{A}$, write
$\mathds{A}\models\varphi[\alpha]$ if $\alpha$ {\em satisfies}
$\varphi$ in $\mathds{A}$ in the standard way. In particular, if
$\varphi$ is a sentence, simply write $\mathds{A}\models\varphi$, and say
$\mathds{A}$ is a {\em model} of $\varphi$, or in other
words, $\varphi$ {\em is true} in $\mathds{A}$. Given formulas $\varphi,\psi$ and a class $\mathcal{C}$ of structures, we say $\varphi$ is {\em equivalent} to $\psi$ over $\mathcal{C}$, or write $\varphi\equiv_{\mathcal{C}}\psi$ for short, if for every $\mathds{A}$ in $\mathcal{C}$ and every assignment $\alpha$ in $\mathds{A}$, $\alpha$ satisfies $\varphi$ in $\mathds{A}$ if and only if $\alpha$ satisfies $\psi$ in $\mathds{A}$. Given a quantifier-free formula $\varphi$
and an assignment $\alpha$ in $\mathds{A}$, let $\varphi[\alpha]$ denote the {\em ground formula} obtained from $\varphi$ by substituting $a$ for $t$ whenever $a=\alpha(t)$ and $t$ is a term.
%
%Given a set $\tau$ of predicates and a nonempty set $A$, let $\textsc{ga}(\tau,A)$ denote the set of $P(\bar{a})$ for all predicates $P\in\tau$ and all $n$-tuples $\bar{a}$ on $A$ where $n$ is the arity of $P$. Let $\textsc{gpc}(\tau,A)$ be the set of finite disjunctions built from atoms in $\textsc{ga}(\tau,A)$. Each element in $\textsc{ga}(\tau,A)$ ($\textsc{gpc}(\tau,A)$) is called a {\em grounded atom} ({\em grounded positive clause}) of $\tau$ over $A$. Given a structure $\mathds{A}$, let $\textsc{Ins}(\mathds{A},\tau)$ be the set of grounded atoms $P(\bar{a})$ such that $P\in\tau$ and $P(\bar{a})$ is true in $\mathds{A}$.

%For the propositional case, a slightly stronger version of the above proposition is still true. A {\em positive clause} is defined to be a finite disjunction of atoms. Given a vocabulary $\upsilon$, let $\textsc{pc}(\upsilon)$ be the set of all positive clauses of $\upsilon$. %Now, we give the following property without a proof since it is in fact the same as that of Theorem 1.2.16 in~\cite{CK:90}.

%grounded atom, grounded positive clauses, $\textsc{gpc}(A,\tau)$

A class of structures is also called a {\em property}. Let $\mathcal{C}$ and $\mathcal{D}$ be two properties. We say $\mathcal{D}$ is {\em defined} by a sentence $\varphi$ over $\mathcal{C}$, or equivalently, $\varphi$ {\em defines} $\mathcal{D}$ over $\mathcal{C}$, if each structure of $\mathcal{C}$ is in $\mathcal{D}$ if and only if it is a model of $\varphi$; $\mathcal{D}$ is {\em definable} in a class $\Sigma$ of sentences over $\mathcal{C}$ if there is a sentence in $\Sigma$ that defines $\mathcal{D}$ over $\mathcal{C}$. Given two classes $\Sigma,\Lambda$ of sentences, we write $\Sigma\leq_{\mathcal{C}}\Lambda$ if each property definable in $\Sigma$ over $\mathcal{C}$ is also definable in $\Lambda$ over $\mathcal{C}$; we write $\Sigma\simeq_{\mathcal{C}}\Lambda$ if both $\Sigma\leq_{\mathcal{C}}\Lambda$ and $\Lambda\leq_{\mathcal{C}}\Sigma$ hold. In particular, if $\mathcal{C}$ is the class of arbitrary structures, the subscript $\mathcal{C}$ can be dropped.%\vspace{-.15cm}


\subsection{Logic Programs and Stable Models}

Every {\em disjunctive program} is a set of {\em rules} of the form%\vspace{-.1cm}
\begin{equation}\label{eqn:rule}
\zeta_1\wedge\cdots\wedge\zeta_{m}\rightarrow\zeta_{m+1}\vee\cdots\vee\zeta_{n}%\vspace{-.1cm}
\end{equation}
where $0\leq m\leq n$ and $n>0$; $\zeta_i$ is an atom not involving the equality if $m<i\leq n$; $\zeta_j$ is a {\em literal}, i.e. an atom or the negation of an atom, if $1\leq j\leq m$. Given a rule, the disjunctive part is called its {\em head}, and the conjunctive part is called its {\em body}. Given a disjunctive program $\Pi$, a predicate is called {\em intensional} (w.r.t. $\Pi$) if it appears in the head of some rule in $\Pi$; a formula is called {\em intensional} (w.r.t. $\Pi$) if it does not involve any non-intensional predicate. Let $\upsilon(\Pi)$ be the set of predicates and functions appearing in $\Pi$.

Let $\Pi$ be a disjunctive program. Then $\Pi$ is called {\em normal} if the head of each rule contains at most one atom, $\Pi$ is {\em plain} if the negation of any intensional atom does not appear in the body of any rule,
$\Pi$ is {\em propositional} if it does not involve any predicate of positive arity, and $\Pi$ is {\em finite} if it contains only a finite set of rules. In particular, unless mentioned otherwise, a disjunctive program is always {\em assumed to be finite}.

%The following is a brief review of the general stable model semantics for logic programs. For each predicate constant $P$ we introduce a new predicate variable $P^{\ast}$ of the
%same arity.
Given any disjunctive program $\Pi$, let $\mathrm{SM}(\Pi)$ denote the second-order sentence
$\varphi\wedge\forall\tau^{\ast}(\tau^{\ast}<\tau\rightarrow\neg\varphi^{\ast})$,
where $\tau$ is the set of intensional predicates; $\tau^{\ast}$ is the set of predicate variables $P^{\ast}$ for all predicates $P$ in $\tau$; $\tau^{\ast}<\tau$ is the formula
$\wedge_{P\in\tau}\forall\bar{x}(P^{\ast}(\bar{x})\rightarrow P(\bar{x}))\wedge\neg\wedge_{P\in\tau}\forall\bar{x}(P(\bar{x})\rightarrow P^{\ast}(\bar{x}))$;
$\varphi$ is the conjunction of all the sentences $\gamma${\small$_{\forall}$} such that $\gamma$ is a rule in $\Pi$ and $\gamma${\small$_{\forall}$} is the first-order universal closure of $\gamma$; $\varphi^{\ast}$ is the formula obtained from $\varphi$ by substituting $P^{\ast}$ for all positive occurrences of $P$ in the head or in the body of each rule if $P$ is in $\tau$. (So, all negations in intensional literals are default negations.) A structure $\mathds{A}$ is called a {\em stable model} of $\Pi$ if it satisfies $\mathrm{SM}(\Pi)$. For more details about this transformation, please refer to~\cite{FLL:11}.

Given two properties $\mathcal{C}$ and $\mathcal{D}$, we say $\mathcal{D}$ is {\em defined} by a disjunctive program $\Pi$ over $\mathcal{C}$ via the set $\tau$ of {\em auxiliary constants} if the formula $\exists\tau\mathrm{SM}(\Pi)$ defines $\mathcal{D}$ over $\mathcal{C}$, where $\tau$ is a set of predicates and functions occurring in $\Pi$. Given $n\geq 0$, let $\mathrm{DLP}_n$ (respectively, $\mathrm{DLP}_n^{\textsc{f}}$) be the class of sentences $\exists\tau\mathrm{SM}(\Pi)$ for all disjunctive programs $\Pi$ and all finite sets $\tau$ of predicate (respectively, predicate and function) constants of arities $\leq n$. Let $\mathrm{DLP}$ (respectively, $\mathrm{DLP}^{\textsc{f}}$) be the union of $\mathrm{DLP}_n$ (respectively, $\mathrm{DLP}_n^{\textsc{f}}$) for all $n\geq 0$. In above definitions, if $\Pi$ is restricted to be normal, we then obtain the notations $\mathrm{NLP}_n,\mathrm{NLP}_n^{\textsc{f}},\mathrm{NLP}$ and $\mathrm{NLP}^{\textsc{f}}$ respectively.

%. Let $\Pi$ be a finite disjunctive logic program $\Pi$ and let $\tau$ be the set of all intensional predicates of $\Pi$, we let
%$\textsc{Circ}(\Pi)$ and $\textsc{SM}(\Pi)$ denote the formulas $\textsc{Circ}(\Pi;\tau)$ and $\textsc{SM}(\Pi;\tau)$ respectively. Every $\tau$-minimal ($\tau$-stable) model of $\Pi$ is simply called a {\em minimal (stable) model of $\Pi$}. It is easy to see that $\textsc{SM}(\Pi)$ is equivalent to $\textsc{Circ}(\Pi)$ is $\Pi$ is plain.

Given a rule $\gamma$, let $\gamma${\small$^-_{\textsc{B}}$} be the set of conjuncts in the body of $\gamma$ in which no intensional predicate positively occurs, and let $\gamma${\small$^+$} be the rule obtained from $\gamma$ by removing all literals in $\gamma${\small$^-_{\textsc{B}}$}. Given a disjunctive program $\Pi$ and a structure $\mathds{A}$, let $\Pi${\small$^{\mathds{A}}$} be the set of rules $\gamma${\small$^{+}[\alpha]$} for all assignments $\alpha$ in $\mathds{A}$ and all rules $\gamma$ in $\Pi$ such that $\alpha$ satisfies $\gamma${\small$^-_{\textsc{b}}$} in $\mathds{A}$. Now, $\Pi^{\mathds{A}}$ can be regarded as a propositional program where each ground atom as a proposition. This procedure is called the {\em first-order Gelfond-Lifschitz reduction} due to the following result:

\begin{prop}[\cite{ZZ:13}, Proposition 4]\label{prop:fo2prop}
Let $\Pi$ be a disjunctive program and $\tau$ the set of intensional predicates. Then an $\upsilon(\Pi)$-structure $\mathds{A}$ is a stable model of $\Pi$ iff $\textsc{Ins}(\mathds{A},\tau)$ is a minimal (w.r.t. the set inclusion) model of $\Pi^{\mathds{A}}$.
\end{prop}%\vspace{-.15cm}
%
%\begin{proof}
%Similar to Theorem 1 in \cite{FLL:11}.
%\end{proof}



\subsection{Progression Semantics}

In this subsection, we review a progression semantics proposed by~\cite{ZZ:13}, which generalizes the fixed point semantics of~\cite{LMR:92} to logic programming with default negation over arbitrary structures. For convenience, two positive clauses consisting of the same set of atoms will be regarded as the same.

%Let $\Pi$ be a disjunctive logic program over $\sigma$ and let $\mathcal{A}$ be a $\sigma$-structure.
%
%Let $\sigma$ be a programming vocabulary and $A$ an arbitrary set. If $P$ is an $n$-ary predicate in $\sigma_{\mathrm{int}}$ and $a_1,\dots,a_n\in A$, we call $P(a_1,\dots,a_n)$ an {\em instantiated atom} of $\sigma$ over $A$. Any finite set of such instantiated atom is said to be an {\em instantiated clause} of $\sigma$ over $A$. An ordered pair $\mathds{A}=(\mathcal{A},I)$ is called a {\em disjunctive structure  of $\sigma$} if $\mathcal{A}$ is a structure of $\sigma_{\mathrm{ext}}$, and $I$ is a set of instantiated clauses of $\sigma$ over $A$.

%\begin{defn}
\smallskip
Let $\Pi$ be a propositional, possibly infinite and plain disjunctive program. Let $\textsc{pc}(\upsilon(\Pi))$ denote the set of positive clauses of $\upsilon(\Pi)$ and let $\Lambda\subseteq\textsc{pc}(\upsilon(\Pi))$. Define $\Gamma_{\Pi}(\Lambda)$ to be%\vspace{-.1cm}
%to be the set of positive clauses $H\vee C_1\vee\cdots\vee C_k$ such that $k\geq 0$ and there exist a rule $p_1\wedge\cdots\wedge p_k\rightarrow H$ in $\Pi$ and a sequence of positive clauses $C_1\vee p_1,\dots,C_k\vee p_k$ in $\Sigma$. It is easy to verify that $\Gamma_{\Pi}$ is a monotonic function on the sets of positive clauses of $\upsilon(\Pi)$.
{\small
\begin{equation*}
\left\{H\vee C_1\vee\cdots\vee C_k\left|
\begin{aligned}
k\ge 0&\,\,\&\,\,H,C_1,\dots,C_k\in\textsc{pc}(\upsilon(\Pi))\\
&\,\,\&\,\,\exists p_1,\dots,p_k\in\upsilon(\Pi)\text{ s.t. } \\
&
\,\left[
\begin{aligned}
&p_1\wedge\cdots\wedge p_k\rightarrow H\in\Pi\,\,\&\\
&C_1\vee p_1,\dots,C_k\vee p_k\in\Lambda
\end{aligned}
\right]
\end{aligned}
\right.
\right\}.
\end{equation*}
}

%\vspace{-.25cm}
\noindent It is clear that $\Gamma_{\Pi}$ is a monotone operator on $\textsc{pc}(\upsilon(\Pi))$.

Now, a progression operator for first-order programs can then be defined via the first-order Gelfond-Lifschitz reduction. Given a disjunctive program $\Pi$ and an $\upsilon(\Pi)$-structure $\mathds{A}$, define  $\Gamma${\small$^{\mathds{A}}_{\Pi}$} to be the operator $\Gamma_{\Pi^{\mathds{A}}}$; let $\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_0$ denote the empty set, and let $\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_n$ denote $\Gamma${\small$^{\mathds{A}}_{\Pi}($}$\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{n-1})$ for all $n>0$; finally, let $\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\omega}$ be the union of $\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_n$ for all $n\geq 0$. To illustrate the definitions, a simple example is given as follows.


\begin{exm}
Let $\Pi$ be the logic program consisting of rules%\vspace{-.1cm}
\begin{equation*}
S(x)\vee T(x)\quad\text{and}\quad T(x)\wedge E(x,y)\rightarrow T(y).%\vspace{-.1cm}
\end{equation*}
Let $\upsilon$ be $\{E\}$ and $\mathds{A}$ a structure of $\upsilon$. Then, for $n>0$, $\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_n$ is the set of clauses $S(a)\vee T(b)$ such that $a,b\in A$ and there exists a path from $a$ to $b$ via $E$ of length less than $n$.\hfill$\Box$%\vspace{.1cm}
\end{exm}

The following proposition shows that the general stable model semantics can be defined by the progression operator.


\begin{prop}[\cite{ZZ:13}, Theorem 1]\label{prop:fxp2sm}
Let $\Pi$ be a disjunctive program, $\tau$ the set of intensional predicates of $\Pi$, and $\mathds{A}$ a structure of $\upsilon(\Pi)$. Then
$\mathds{A}$ is a stable model of $\Pi$ iff $\textsc{Ins}(\mathds{A},\tau)$ is a minimal model of $\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\omega}$.
\end{prop}


\begin{rem}
In Proposition \ref{prop:fxp2sm}, it is clear that, if $\Pi$ is normal, $\mathds{A}$ is a stable model of $\Pi$ if and only if $\textsc{Ins}(\mathds{A},\tau)=\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\omega}$.
\end{rem}


%\subsection{Fixpoint Theory}
%
%A partially ordered set $L$ is a {\em complete lattice} if $lub(X)$ and $glb(X)$ exist for every subset $X$ of $L$.
%
%\begin{prop}
%Let $\Pi$ be a disjunctive logic program. Then $\langle\textsc{pc}(\upsilon(\Pi)),\subseteq\rangle$ is a complete lattice.
%\end{prop}
%
%
%Let $L$ be a complete lattice. A subset $X$ of $L$ is called a {\em directed set} if every finite subset of $X$ has an upper bound in $X$. Let $\Gamma: L\rightarrow L$ be a mapping. Then $\Gamma$ is monotonic if for all $a_1,a_2\in L$, $a_1\le a_2$ implies $\Gamma(a_1)\le\Gamma(a_2)$, and $\Gamma$ is {\em continuous} if $\Gamma(lub(X))=lub\{\Gamma(a):a\in X\}$.
%
%\begin{prop}
%Let $\Pi$ be a disjunction logic program, and $\mathds{A}$ an arbitrary structure of the same vocabulary. Then $\Gamma^{\mathds{A}}_{\Pi}$ is a continuous and monotonic operator on $\textsc{pc}(\upsilon(\Pi))$.
%\end{prop}
%
%\begin{proof}
%
%\end{proof}
%
%
%\begin{thm}
%$lfp(\Gamma^{\mathds{A}}_{\Pi})=\Gamma^{\mathds{A}}_{\Pi}\uparrow_{\omega}$.
%\end{thm}

\section{Infinite Structures}

This section will focus on the expressiveness of logic programs over infinite structures. We first propose a translation that reduces each disjunctive program to a normal program over infinite structures. The main idea is to encode grounded positive clauses by elements in the intended domain. With the encoding, we then simulate the progression of the given disjunctive program by the progression of a normal program.

\smallskip
We first show how to encode a positive clause by an element.
Let $A$ be an infinite set. Each {\em encoding function} on $A$ is defined to be an injective function from $A\times A$ into $A$. Let $\textsl{enc}$ be an encoding function on $A$ and $c$ an element in $A$ such that $\textsl{enc}(a,b)\neq c$ for all elements $a,b\in A$. To simplify the statement, let $\textsl{enc}(a_1,\dots,a_k;c)$ denote the expression%\vspace{-.1cm}
\begin{equation}
\textsl{enc}((\cdots(\textsl{enc}(c,a_1),a_2),\cdots),a_k)%\vspace{-.1cm}
\end{equation} for any $k\geq 0$ and any set of elements $a_1,\dots,a_k\in A$. In the above expression, the special element $c$ is used as a flag to indicate that the encoded tuple will be started after $c$, and is then called the {\em encoding flag} of this encoding.

Let $A^{\ast}$ denote the set of finite tuples of elements in $A$ and $\textsl{enc}[A,c]$ the set of elements $\textsl{enc}(\bar{a};c)$ for all tuples $\bar{a}$ in $A^{\ast}$. The {\em merging function} $\textsl{mrg}$ on $A$ related to $\textsl{enc}$ and $c$ is the function from $\textsl{enc}[A,c]\times\textsl{enc}[A,c]$ into $\textsl{enc}[A,c]$ such that%\vspace{-.1cm}
\begin{equation}
\textsl{mrg}(\textsl{enc}(\bar{a};c),\textsl{enc}(\bar{b};c))=\textsl{enc}(\bar{a},\bar{b};c)%\vspace{-.1cm}
\end{equation}
for all tuples $\bar{a}$ and $\bar{b}$ in $A^{\ast}$. Again, to simplify the statement, we let $\textsl{mrg}(a_1,\dots,a_k)$ be short for the expression%\vspace{-.1cm}
\begin{equation}
\textsl{mrg}((\cdots(\textsl{mrg}(a_1,a_2),a_3),\cdots),a_k)%\vspace{-.1cm}
\end{equation}
if all encoding flags of $a_1,\dots,a_k$ are the same.
%The {\em extracting function} $\textsl{ext}$ on $A$ related to $\textsl{enc}$ and $c$ is the function from $\textsl{enc}(A,c)\times A$ into $\textsl{enc}(A,c)$ that satisfies $\textsl{ext}(\textsl{enc}(\bar{a};c),b)=\textsl{enc}(\bar{a}';c)$, where $\bar{a}'$ is the tuple obtained from $\bar{a}$ by removing all occurrences of $b$. It is clear that both the merging function and the extracting function are unique if $\textsl{enc}$ and $c$ are fixed.
It is clear that the merging function is unique if $\textsl{enc}$ and $c$ are fixed.


\begin{exm}
Let $\mathbb{Z}^+$, the set of all positive integers, be the domain that we will focus, and let $P_1,P_2,P_3$ be three  predicates of arities $2,3,1$ respectively. Next, we show how to encode ground positive clauses by integers in $\mathbb{Z}^+$.

Let $e$ be a function from $\mathbb{Z}^+\times\mathbb{Z}^+$ into $\mathbb{Z}^+$ such that%\vspace{-.1cm}
\begin{equation}
e(m,n)=2^{m}+3^{n}\text{ for all }m,n\in\mathbb{Z}^+.%\vspace{-.1cm}
\end{equation}
It is easy to check that $e$ is an encoding function on $\mathbb{Z}^+$, and integers $1,2,3,4$ are not in the range of $e$. For $1\le i\le 3$, let $i$ be the encoding flag for the encodings of atoms built from $P_i$. Then the grounded atom $P_2(1,3,5)$ can be encoded by%\vspace{-.1cm}
\begin{equation}
e(1,3,5;2)=e(e(e(2,1),3),5)=2^{155}+3^5.%\vspace{-.1cm}
\end{equation}
Let $4$ be the encoding flag for encodings of positive clauses. Then the positive clause $P_2(1,3,5)\vee P_3(2)\vee P_1(2,4)$ can be encoded by $e(e(1,3,5;2),e(2;3),e(2,4;1);4)$.\hfill$\Box$%\vspace{.1cm}
%\smallskip
\end{exm}

In classical logic, two positive clauses are equivalent if and only if they contain the same set of atoms. Assume that $c$ is the encoding flag for encodings of positive clauses and $\textsl{enc}$ is the encoding function. To capture the equivalence between two positive clauses, some encoding predicates related to $\textsl{enc}$ and $c$ are needed. We define them as follows:%\vspace{-.1cm}%\footnote{To simplify the statement, given a tuple $\bar{a}$ of elements, we regard it as the set consisting of all the elements appearing in $\bar{a}$.}:
%The first relation is $\textsl{in}$, a subset of $\textsl{enc}[A,c]\times A$ defined by that $(\textsl{enc}(\bar{a},c),b)\in\textsl{in}$ if and only if $b$ has at least one occurrence in $\bar{a}$. The second one, $\textsl{subc}$, is a binary relation on $\textsl{enc}[A,c]$ such that $(\textsl{enc}(\bar{a},c),\textsl{enc}(\bar{b},c))\in\textsl{subc}$ if and only if all the elements in $\bar{a}$ occur in $\bar{b}$. The third one $\textsl{equ}$ is also a binary relation on $\textsl{enc}[A,c]$ such that
%$(a,b)\in\textsl{equ}$ if and only if $(a,b)\in\textsl{subc}$ and $(b,a)\in\textsl{subc}$.
\begin{eqnarray}
\label{eqn:defn_in}\!\!\!\!\textsl{in}\!\!\!\!&=&\!\!\!\!\{(\textsl{enc}(\bar{a};c),b)\mid\bar{a}\in A^{\ast}\wedge b\in[\bar{a}]\},\\
\label{eqn:defn_subc}\!\!\!\!\textsl{subc}\!\!\!\!&=&\!\!\!\!\{(\textsl{enc}(\bar{a};c),\textsl{enc}(\bar{b};c))\mid\bar{a},\bar{b}\in A^{\ast}\wedge[\bar{a}]\subseteq[\bar{b}]\},\\
\label{eqn:defn_equ}\!\!\!\!\textsl{equ}\!\!\!\!&=&\!\!\!\!\{(\textsl{enc}(\bar{a};c),\textsl{enc}(\bar{b};c))\mid\bar{a},\bar{b}\in A^{\ast}\wedge[\bar{a}]=[\bar{b}]\},%\vspace{-.1cm}
\end{eqnarray}
where $[\bar{a}],[\bar{b}]$ are the sets of elements in $\bar{a},\bar{b}$ respectively. %if $\bar{a}\in A^{\ast}$.
%Please note that, in above definitions, we regard each tuple $\bar{a}$ as same as
Intuitively, $\textsl{in}(a,b)$ expresses that the atom encoded by $b$ appears in the positive clause encoded by $a$; $\textsl{subc}(a,b)$ expresses that the positive clause encoded by $a$ is a subclause of that encoded by $b$; and $\textsl{equ}(a,b)$ expresses that the positive clauses encoded by $a$ and $b$ respectively are equivalent.

\smallskip
With the above method for encoding, we can then define a translation.
Let $\Pi$ be a disjunctive program. We first construct a class of normal programs related to $\Pi$ as follows:

\smallskip

1. Let $C_{\Pi}$ denote the set consisting of an individual constant $c_{P}$ for each predicate constant $P$ that occurs in $\Pi$, and of an individual constant $c_{\epsilon}$, where $c_{\epsilon}$ will be interpreted as the encoding flag for positive clauses, and $c_P$ as the encoding flag for atoms built from $P$. Let $\Pi_1$ consist of the rule
\begin{eqnarray}
\label{eqn:pi1_1}\textsc{enc}(x,y,c)&\rightarrow&\bot
\end{eqnarray}
for each individual constant $c\in C_{\Pi}$, and the following rules:
\begin{eqnarray}
\label{eqn:pi1_2}\!\!\!\!\!\!\!\!\!\!\neg\underline{\textsc{enc}}(x,y,z)\!\!\!\!&\rightarrow&\!\!\!\!\textsc{enc}(x,y,z)\\
\label{eqn:pi1_3}\!\!\!\!\!\!\!\!\!\!\neg\textsc{enc}(x,y,z)\!\!\!\!&\rightarrow&\!\!\!\!\underline{\textsc{enc}}(x,y,z)\\
\label{eqn:pi1_4}\!\!\!\!\!\!\!\!\!\!\textsc{enc}(x,y,z)\wedge\textsc{enc}(u,v,z)\wedge\neg x=u\!\!\!\!&\rightarrow&\!\!\!\!\bot\\
\label{eqn:pi1_5}\!\!\!\!\!\!\!\!\!\!\textsc{enc}(x,y,z)\wedge\textsc{enc}(u,v,z)\wedge\neg y=v\!\!\!\!&\rightarrow&\!\!\!\!\bot\\
\label{eqn:pi1_6}\!\!\!\!\!\!\!\!\!\!\textsc{enc}(x,y,z)\!\!\!\!&\rightarrow&\!\!\!\!\textsc{ok}_e(x,y)\\
\label{eqn:pi1_7}\!\!\!\!\!\!\!\!\!\!\neg\textsc{ok}_e(x,y)\!\!\!\!&\rightarrow&\!\!\!\!\textsc{ok}_e(x,y)\\
\label{eqn:pi1_8}\!\!\!\!\!\!\!\!\!\!\textsc{enc}(x,y,z)\wedge\textsc{enc}(x,y,u)\wedge\neg z=u\!\!\!\!&\rightarrow&\!\!\!\!\bot
\end{eqnarray}%%\vspace{-.5cm}
Informally, rules (\ref{eqn:pi1_6})--(\ref{eqn:pi1_8}) describe that $\textsc{enc}$ is the graph of a function; rules (\ref{eqn:pi1_4})--(\ref{eqn:pi1_5}) describe that $\textsc{enc}$ is injective. Thus, $\textsc{enc}$ should be the graph of an encoding function. In addition, rule (\ref{eqn:pi1_1}) assures that $c$ is not in the range of $\textsc{enc}$.


\smallskip
2. Let $\Pi_2$ be the program consisting of the following rules:%%\vspace{-.15cm}
\begin{eqnarray}
\label{eqn:pi2_1}\!\!\!\!\!\!\!\!y=c_{\epsilon}\!\!\!\!&\rightarrow&\!\!\!\!\textsc{mrg}(x,y,x)\\
%\!\!\!\!\!\!\!\!\textsc{in}(y,x)\!\!\!\!&\rightarrow&\!\!\!\!\textsc{mrg}(x,y,x)\\
\label{eqn:pi2_2}\!\!\!\!\!\!\!\!\left[\begin{aligned}
\textsc{mrg}(x,u,v)&\wedge\textsc{enc}(u,w,y)\\
&\wedge\textsc{enc}(v,w,z)
\end{aligned}\right]
\!\!\!\!\!\!&\rightarrow&\!\!\!\!\textsc{mrg}(x,y,z)\\
%\!\!\!\!\!\!\!\!x=c_{\epsilon}\!\!\!\!&\rightarrow&\!\!\!\!\textsc{ext}(x,y,x)\\
%\!\!\!\!\!\!\!\!\textsc{ext}(u,y,v)\wedge\textsc{enc}(u,w,x)\wedge w=y\!\!\!\!&\rightarrow&\!\!\!\!\textsc{ext}(x,y,v)\\
%\!\!\!\!\!\!\!\!\left[\begin{aligned}
%\textsc{ext}(u,y,v)\wedge\textsc{enc}(u,w,x)\\
%\wedge \neg w=y\wedge\textsc{enc}(v,w,z)
%\end{aligned}\right]
%\!\!\!\!\!\!&\rightarrow&\!\!\!\!\textsc{ext}(x,y,z)\\
\label{eqn:pi2_3}\!\!\!\!\!\!\!\!\textsc{enc}(x,u,y)\!\!\!\!&\rightarrow&\!\!\!\!\textsc{in}(u,y)\\
\label{eqn:pi2_4}\!\!\!\!\!\!\!\!\textsc{enc}(x,z,y)\wedge\textsc{in}(u,x)\!\!\!\!&\rightarrow&\!\!\!\!\textsc{in}(u,y)\\
\label{eqn:pi2_5}\!\!\!\!\!\!\!\!x=c_{\epsilon}\!\!\!\!&\rightarrow&\!\!\!\!\textsc{subc}(x,y)\\
\label{eqn:pi2_6}\!\!\!\!\!\!\!\!\!\!\textsc{subc}(u,y)\wedge\textsc{enc}(u,v,x)\wedge\textsc{in}(v,y)\!\!\!\!&\rightarrow&\!\!\!\!\textsc{subc}(x,y)\\
\label{eqn:pi2_7}\!\!\!\!\!\!\!\!\!\!\textsc{subc}(x,y)\wedge\textsc{subc}(y,x)\!\!\!\!&\rightarrow&\!\!\!\!\textsc{equ}(x,y)
\end{eqnarray}%%\vspace{-.5cm}
Informally, rules (\ref{eqn:pi2_1})--(\ref{eqn:pi2_2}) describe that $\textsc{mrg}$ is the graph of the merging function related to $\textsc{enc}$ and $c_{\epsilon}$; rules (\ref{eqn:pi2_3})--(\ref{eqn:pi2_4}) are an inductive version of  (\ref{eqn:defn_in}); rules (\ref{eqn:pi2_5})--(\ref{eqn:pi2_6}) are an inductive version of (\ref{eqn:defn_subc}); all rules (\ref{eqn:pi2_3})--(\ref{eqn:pi2_7}) then assert that $\textsc{equ}$ is the equivalence between positive clauses.


\smallskip
3. Let $\Pi_3$ be the logic program consisting of the rule%%\vspace{-.15cm}
\begin{eqnarray}
\label{eqn:pi3_equtran}
\textsc{true}(x)\wedge\textsc{equ}(x,y)&\rightarrow&\textsc{true}(y)
\end{eqnarray}%%\vspace{-.55cm}
and the rule%%\vspace{-.15cm}
{\small
\begin{eqnarray}
\label{eqn:pi3_progsim}
\!\!\!\!\!\!\!\!\!\!\!\left[\begin{aligned}
&\textsc{true}(x_1)\wedge\cdots\wedge\textsc{true}(x_k)\,\wedge\\
%&\textsc{in}(\lceil\vartheta_1\rceil,x_1)\wedge\cdots
%\wedge\textsc{in}(\lceil\vartheta_k\rceil,x_k)\,\wedge\\
&\textsc{enc}(y_1,\lceil\vartheta_1\rceil,x_1)
\wedge\cdots\wedge\textsc{enc}(y_k,\lceil\vartheta_k\rceil,x_k)\\
&\qquad\qquad\,\,\,\,\wedge\textsc{mrg}(\lceil\gamma_{\textsc{h}}\rceil,y_1,\dots,y_k,z)\wedge\gamma^{\overline{\mbox{ }\!\mbox{ }}}_{\textsc{b}}\end{aligned}\right]
\!\!\!\!\!\!\!&\rightarrow&\!\!\!\!\!\textsc{true}(z)
\end{eqnarray}%%\vspace{-.25cm}
}
%\vspace{-.2cm}

\noindent
for each rule $\gamma$ in $\Pi$, where $\vartheta_1,\dots,\vartheta_k$ list all the intensional atoms that have strictly positive occurrences in the body of $\gamma$ for some $k\geq 0$; $\gamma_{\textsc{h}}$ is the head of $\gamma$, $\gamma^-_{\textsc{b}}$ is the conjunction of literals occurring in the body of $\gamma$ but not in $\vartheta_1,\dots,\vartheta_k$; $\textsc{enc}(t_1,\lceil\vartheta\rceil,t_2)$ denotes the following conjunction%%\vspace{-.15cm}
\begin{align*}
u^i_0=c_P\,\wedge\,&\textsc{enc}(u^i_0,t_1,u^i_1)\wedge\cdots\\
&\wedge\textsc{enc}(u^i_{m-1},t_m,u^i_m)\wedge\textsc{enc}(t_1,u^i_m,t_2)
\end{align*}%%\vspace{-.55cm}
for some new variables $u^i_j$ if $t_1,t_2$ are terms and $\vartheta$ an atom of form $P(t_1,\dots,t_m)$;  $\textsc{mrg}(\lceil\gamma_{\textsc{h}}\rceil,y_1,\dots,y_k,z)$ denotes%%\vspace{-.15cm}
\begin{align*}
\textsc{enc}(v_0,&\lceil\zeta_1\rceil,v_1)\wedge\cdots\wedge\textsc{enc}(v_{n-1},\lceil\zeta_n\rceil,v_n)\\
&\wedge\textsc{mrg}(w_0,y_1,w_1)\wedge\cdots\wedge\textsc{mrg}(w_{k-1},y_k,w_k)\\
&\wedge v_0=c_{\epsilon}\wedge w_0=v_n\wedge z=w_k
\end{align*}%%\vspace{-.55cm}
if $\gamma_{\textsc{h}}=\zeta_1\vee\cdots\vee\zeta_n$ for some atoms $\zeta_1,\dots,\zeta_n$ and $n\geq 0$.

Intuitively, rule (\ref{eqn:pi3_equtran}) assures that the progression is closed under the equivalence of positive clauses; rule (\ref{eqn:pi3_progsim}) then simulates the progression operator for the original program. As each positive clause is encoded by an element in the intended domain, the processes of decoding and encoding should be carried out before and after the simulation respectively.


\begin{exm}
Let $\gamma\!=\!P(v)\wedge\neg Q(v)\rightarrow R(v)\vee S(v)$ be a rule such that $P,Q,R,S$ are intensional. Then the following rule, defined by\! (\ref{eqn:pi3_progsim})\! with a slight simplification, simulates $\gamma$:
{\small
\begin{equation*}
\!\!\left[\begin{aligned}
\!&\textsc{true}(x_1)\wedge\textsc{enc}(c_P,\!v,\!u_1)\wedge\textsc{enc}(y_1,\!u_1,\!x_1)\,\wedge\\
\!&\textsc{enc}(c_R,\!v,\!u_2)\wedge\textsc{enc}(c_{\epsilon},\!u_2,\!w_1)\wedge\textsc{enc}(c_S,\!v,\!u_3)\,\wedge\\
&\quad\,\qquad\textsc{enc}(w_1,\!u_3,\!w_2)\wedge
\textsc{mrg}(w_2,\!y_1,\!z)\wedge\neg Q(v)
\end{aligned}\right]\!\!\rightarrow\!\textsc{true}(z).
\end{equation*}
}
\end{exm}

\smallskip
4. Let $\Pi_4$ be the program consisting of the rule%%\vspace{-.15cm}
\begin{eqnarray}
\label{eqn:pi4_false1}x=c_{\epsilon}&\rightarrow&\textsc{false}(x)
\end{eqnarray}%%\vspace{-.55cm}
and the rule%%\vspace{-.15cm}
\begin{eqnarray}
\label{eqn:pi4_false2}\!\!\!\!\!\!\!\textsc{false}(x)\wedge\textsc{enc}(x,\lceil\vartheta\rceil,y)\wedge\neg\vartheta\!\!\! &\rightarrow&\!\!\! \textsc{false}(y)
\end{eqnarray}%%\vspace{-.55cm}
for every intensional atom $\vartheta$ of the form $P(\bar{z}_P)$, where $\bar{z}_P$ denotes a tuple of distinct individual variables $z_1\cdots z_{k_P}$ that are different from $x$ and $y$, and $k_P$ is the arity of $P$.

This program is intended to define the predicate $\textsc{false}$ as follows: $\textsc{false}(a)$ holds in the intended structure if and only if $a$ encodes a positive clause that is false in the structure. %So, rules (\ref{eqn:pi4_false1}) and (\ref{eqn:pi4_false2}) are then


\smallskip
5. Let $\Pi_5$ be the logic program consisting of the rule%%\vspace{-.15cm}
\begin{eqnarray}
\label{eqn:pi5_true1}\textsc{true}(c_{\epsilon})&\rightarrow&\bot
\end{eqnarray}%%\vspace{-.55cm}
and the following rule%%\vspace{-.15cm}
\begin{eqnarray}
\label{eqn:pi5_true2}\!\!\!\!\!\!\!\textsc{true}(x)\wedge\textsc{enc}(y,\lceil\vartheta\rceil,x)\wedge\textsc{false}(y)\!\!\! &\rightarrow&\!\!\!\vartheta
\end{eqnarray}%%\vspace{-.55cm}
for each atom $\vartheta$ of the form same as that in $\Pi_4$.

Informally, this program asserts that a ground atom is true in the intended structure if and only if there is a positive clause containing this atom such that the clause in true and all the other atoms in this clause are false in the structure.

\smallskip
Now, we let $\Pi^{\diamond}$ denote the union of $\Pi_1,\dots,\Pi_5$. This then completes the definition of the translation. The soundness of this translation is assured by the following theorem.


%Next, we explain the intuition of this translation. Program $\Pi_1$ assures that $\textsc{enc}$ will be interpreted as an encoding function on the domain and constants in $C_{\Pi}$ will be interpreted as ending flags for the encoding of atoms and positive clauses. Program $\Pi_2$ defines the merging and extracting functions, and all the encoding predicates mentioned before. Based on these assumptions, program $\Pi_3$ then simulates the progression of $\Pi$ on encodings of positive clauses. As all the needed clauses will be derived in $\omega$ stages, this simulation is realizable. Lastly, we use program $\Pi_5$ and $\Pi_4$ to decode the encodings of positive clauses. The only difficulty in this decoding is that we need represent the resulting positive clauses by a program without disjunction. As the set of positive clauses are clearly head-cycle-free, we can get over it by applying the shift operation presented in~\cite{BD:94}.

\begin{thm}\label{thm:tran_infinite}
Let $\Pi$ be a disjunctive program. Then over infinite structures, $\textsc{SM}(\Pi)$ is equivalent to $\exists\pi\textsc{SM}(\Pi^{\diamond})$, where $\pi$ denotes the set of constants occurring in $\Pi^{\diamond}$ but not in $\Pi$.
\end{thm}

To prove this result, some notations and lemmas are needed.
%Let $\tau$ be the set of intensional predicates of $\Pi$, and let $\sigma$ be the union of
Let $\upsilon_i$ and $\tau$ be the sets of intensional predicates of $\Pi_i$ and $\Pi$ respectively. Let $\sigma=\upsilon_1\cup\upsilon_2\cup\upsilon(\Pi)$. Given a structure $\mathds{A}$ of $\upsilon(\Pi)$, each {\em encoding expansion} of $\mathds{A}$ is defined to be a $\sigma$-expansion $\mathds{B}$ of $\mathds{A}$ satisfying both of the following:
%is a let $\mathds{A}^+$ denote the\footnote{In fact, there exists many expansions satisfying the above condition. For simplicity, a method to select an expansion from such expansions is assumed to be fixed so that $\mathds{A}^+$ is well-defined.} $\sigma$-expansion $\mathds{B}$ of $\mathds{A}$ satisfying both of following conditions:
\begin{enumerate}
\item $\textsc{enc}$ is interpreted as the graph of an encoding function $\textsl{enc}$ on $A$ such that no element among $c${\small$_{\epsilon}^{\mathds{B}}$} and $c${\small$_P^{\mathds{B}}$} (for all $P\in\tau$) belongs to the range of $\textsl{enc}$, $\underline{\textsc{enc}}$ as the complement of the graph of $\textsl{enc}$, and $\textsc{ok}${\small$_e^{\mathds{B}}$}$=A\times A$;
\item $\textsc{mrg}$ is interpreted as the graph of the merging function related to $\textsl{enc}$ and $c${\small$_{\epsilon}^{\mathds{B}}$}, and $\textsc{in},\textsc{subc},\textsc{equ}$ as the encoding predicates $\textsl{in},\textsl{subc},\textsl{equ}$ related to $\textsl{enc}$ and $c${\small$_{\epsilon}^{\mathds{B}}$} respectively.
\end{enumerate}
%It is clear that $\mathds{B}$ satisfies $\mathrm{SM}(\Pi_i;\upsilon_i)$ for $i=1$ or $2$. On the other hand, we can also verify that

%In this rest of this section, we fix $\mathds{A}$ to be an infinite $\upsilon(\Pi)$-structure, and fix $\textsl{enc},\textsl{mrg},\textsl{in},\textsl{subc},\textsl{equ}$ to be the interpretations in $\mathds{A}^+$ for the corresponding predicates respectively. %As $\mathds{A}$ is infinite, such interpretations always exist.
%
%Now, some notations are defined for the encoding. Given a grounded atom $\vartheta$ of the form $P(a_1,\dots,a_k)$ for any $P\in\tau$, let $[\![\vartheta]\!]$ be short for $\textsl{enc}(a_1,\dots,a_k;c_P^{\mathds{B}})$. Given a grounded clause $C$ in $\textsc{gpc}(\tau,A)$ of the form $\vartheta_1\vee\cdots\vee\vartheta_n$ where each $\vartheta_i$ is an atom, let $[\![C]\!]$ denote $\textsl{enc}([\![\vartheta_1]\!],\dots,[\![\vartheta_n]\!];c_{\epsilon}^{\mathds{B}})$. Given a set $\Sigma\subseteq\textsc{gpc}(\tau,A)$, let $[\![\Sigma]\!]$ denote the set $\{[\![C]\!]\mid C\in\Sigma\}$. Moreover, let $\Delta^{n}(\mathds{B})=\{a\in B\mid\textsc{true}(a)\in\Gamma^{\mathds{B}}_{\Pi_3}\uparrow_n\}$. By an induction on $n$, we can show the following claim:


Let $\mathds{A}$ be a structure of $\upsilon(\Pi)$ with an encoding expansion $\mathds{B}$. Let $\textsl{enc}$ be the encoding function with graph $\textsc{enc}${\small$^{\mathds{B}}$}. Let
\begin{align}
[\![P(a_1\hspace{-0.005in},\hspace{-0.005in}\dots\hspace{-0.005in},\hspace{-0.005in}a_k)]\!]^{\mathds{B}}&=\textsl{enc}(a_1,\dots,a_k;c_P^{\mathds{B}}),\\
[\![\vartheta_1\vee\hspace{0.004in}\cdots\hspace{0.005in}\vee\vartheta_n]\!]^{\mathds{B}}&=\textsl{enc}([\![\vartheta_1]\!]^{\mathds{B}},\dots,[\![\vartheta_n]\!]^{\mathds{B}};c_{\epsilon}^{\mathds{B}}).
\end{align}
If the encoding expansion $\mathds{B}$ is clear from the context, we simply write $[\![\cdot]\!]${\small$^{\mathds{B}}$} as $[\![\cdot]\!]$. Given a set $\Sigma$ of ground positive clauses, let $[\![\Sigma]\!]$ be the set of elements $[\![C]\!]$ for all $C\in\Sigma$. Let $\Delta^n(\mathds{B})$ be the set of elements $a$ with $\textsc{true}(a)\in\Gamma${\small$^{\mathds{B}}_{\Pi_3}$}$\uparrow_n$.


%Moreover, let $\Delta^{n}(\mathds{B})=\{a\in B\mid\textsc{true}(a)\in\Gamma^{\mathds{B}}_{\Pi_3}\uparrow_n\}$.

\begin{lem}\label{lem:progress_sim}
Let $\mathds{A}$ be a structure of $\upsilon(\Pi)$ with an encoding expansion $\mathds{B}$. Then $[\![\Gamma${\small$^{\mathds{A}}_{\Pi}$}$\uparrow_{\omega}]\!]=\cup_{n\ge 0}\Delta${\small$^{n}$}$(\mathds{B})$.
\end{lem}%\vspace{-.05cm}


%\begin{proof}
%%We show it by an induction on $n$. The case of $n=0$ is trivial. Let $n>0$ and assume  $[\![\Gamma^{\mathds{A}}_{\Pi}\uparrow_{n-1}]\!]=\Delta^{2(n-1)}(\mathds{B})$. Now, it remains to show that $[\![\Gamma^{\mathds{A}}_{\Pi}\uparrow_n]\!]=\Delta^{2n}(\mathds{B})$.
%%
%``Subset": By definition, it is sufficient to show that $[\![\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_n]\!]\subseteq\Delta^{2n}(\mathds{B})$ for all $n\ge 0$. We show this by an induction on $n$. The case for $n=0$ is trivial. Let $n>0$ and assume $[\![\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{n-1}]\!]\subseteq\Delta^{2(n-1)}(\mathds{B})$. Now, our task is to show  $[\![\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_n]\!]\subseteq\Delta^{2n}(\mathds{B})$. Let $C\in\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_n$. By definition, there exists a rule $p_1\wedge\cdots\wedge p_k\rightarrow H$, denoted by $\gamma_p$, in $\Pi^{\mathds{A}}$, and a sequence of clauses $C_1\vee p_1,\dots,C_k\vee p_k$ in $\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{n-1}$ such that $C\equiv C'$, where $C'$ denotes $H\vee C_1\vee\cdots\vee C_k$. Consequently, there are a rule $\gamma$ in $\Pi$ and an assignment $\alpha$ in $\mathds{A}$ such that $\alpha$ satisfies $\gamma^-_{\textsc{b}}$ in $\mathds{A}$ and that $\gamma^+[\alpha]=\gamma_p$. Let $a$ denote $[\![C]\!]$ and let $a'$ denote $[\![C']\!]$. Let $a_i$ denote $[\![C_i\vee p_i]\!]$. On the other hand, by the inductive assumption, each $a_i$ should be in $\Delta^{2(n-1)}(\mathds{B})$, or equivalently $\textsc{true}(a_i)\in\Gamma${\small$^{\mathds{B}}_{\Pi_3}$}\,$\uparrow_{2(n-1)}$; by definition, there exists a rule of form (\ref{eqn:pi3_progsim}) related to $\gamma$ in $\Pi_3$. Consequently, we then have that $\textsc{true}(a')\in\Gamma${\small$^{\mathds{B}}_{\Pi_3}$}\,$\uparrow_{2n-1}$. As $\textsc{equ}(a',a)$ is clearly true in $\mathds{B}$, by rule (\ref{eqn:pi3_equtran}) we then have $\textsc{true}(a)\in\Gamma${\small$^{\mathds{B}}_{\Pi_3}$}\,$\uparrow${\small$_{2n}$}, which implies $a\in\Delta^{2n}(\mathds{B})$.
%
%``Superset": It suffices to show that $[\![\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_n]\!]\supseteq\Delta^{n}(\mathds{B})$ for all $n\ge 0$. Similarly, we show it by an induction on $n$. The case for $n=0$ is trivially true. Let $n>0$ and assume that $[\![\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{n-1}]\!]\supseteq\Delta^{n-1}(\mathds{B})$. Let $a\in\Delta^n(\mathds{B})$. We then have $\textsc{true}(a)\in\Gamma${\small$^{\mathds{B}}_{\Pi_3}$}$\uparrow_{n}$. By definition, $\textsc{true}(a)$ must be generated by either rule (\ref{eqn:pi3_equtran}) or rule (\ref{eqn:pi3_progsim}). If the first case is true, there should exist $b\in\Gamma${\small$^{\mathds{B}}_{\Pi_3}$}$\uparrow_{n-1}$ such that $\textsc{equ}(a,b)$ is true in $\mathds{B}$. By the inductive assumption, there is a positive clause $C$ such that $[\![C]\!]=b$ and $C\in\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{n-1}$. By the definition of $\textsl{equ}$, it is also clear that $a$ encodes a clause $C_0$ that contains exactly the set of atoms in $C$. By the definition of the progression operator, it is clear that $C_0\in\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{n-1}\subseteq\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{n}$.
%
%Now, it remains to consider the case that $\textsc{true}(a)$ is generated by rule (\ref{eqn:pi3_progsim}). By definition,
%there should exist (i) a sequence of elements $b_1,\dots,b_k\in B$ with $\textsc{true}(b_i)\in\Gamma${\small$^{\mathds{B}}_{\Pi_3}$}\,$\uparrow_{n-1}$ for each $i$, (ii) a rule $\gamma\in\Pi$ with $\vartheta_1,\dots,\vartheta_k$ are the set of intensional atoms positively appearing in the body, (iii) a sequence of elements $a_1,\dots,a_k\in B$, and (iv) an assignment $\alpha$ in $\mathds{B}$ such that  $\textsc{mrg}([\![H]\!],a_1,\dots,a_k,a)$ and $\textsc{enc}(a_i,[\![p_i]\!],b_i)$ for all $i$ are true in $\mathds{B}$, where $p_i=\vartheta_i[\alpha]$ and $H$ denotes the clause $\gamma_{\textsc{h}}[\alpha]$. By the inductive assumption, there exist a sequence of clauses $C_1\vee p_1,\dots,C_k\vee p_k$ in $\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{n-1}$ such that $[\![C_i\vee p_i]\!]=b_i$ and $[\![C_i]\!]=a_i$. Let $C$ denote $H\vee C_1\vee\cdots\vee C_k$. By definition, $C$ should be in $\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_n$. It is also clear that $a=[\![C]\!]$. This implies  $a\in[\![\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_n]\!]$.
%\end{proof}

Next, given a structure $\mathds{A}$ of $\upsilon(\Pi)$, an $\upsilon(\Pi^{\diamond})$-expansion $\mathds{C}$ of $\mathds{A}$ is called a {\em progression expansion} of $\mathds{A}$ if the restriction of $\mathds{C}$ to $\sigma$, denoted by $\mathds{B}$, is an encoding expansion of $\mathds{A}$; $\mathds{C}$ interprets $\textsc{true}$ as $[\![\Gamma${\small$^{\mathds{A}}_{\Pi}$}$\uparrow_{\omega}]\!]${\small$^{\mathds{B}}$}, and interprets $\textsc{false}$ as%\vspace{-.12cm}
\begin{equation}
\left\{[\![C]\!]^{\mathds{B}}\mid C\in\textsc{gpc}(\tau,A)\,\,\&\,\,\textsc{Ins}(\mathds{A},\tau)\models\neg C\right\}%\vspace{-.12cm}
\end{equation}
where $\textsc{gpc}(\tau,A)$ denotes the set of ground positive clauses built from predicates in $\tau$ and elements in $A$.

%Let $\mathds{D}$ be the $\upsilon_{\leq 4}$-expansion of $\mathds{C}$ that interprets $\textsc{false}$ as the set of  elements $\textsl{enc}(C)$ for all clauses $C\in\textsc{gpc}(\tau,A)$ in which each atom is false in $\mathds{B}$.
%
%Let $\mathds{E}$ be a $\upsilon_{\leq 5}$-expansion of $\mathds{C}$ such that $\textsc{true}$ is interpreted as the set $\{a\in B:\textsc{true}_a\in\Gamma^{\mathds{B}}_{\Pi_4}\uparrow\omega\}$.



%\begin{lem}\label{lem:infinite_a&c}
%Let $\mathds{A}$ be a structure of $\upsilon(\Pi)$ with a progression expansion $\mathds{C}$, and let $M$ be a subset of $\textsc{Ins}(\mathds{A},\tau)$. Then $M$ is a model of $\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\omega}$ iff $M\supseteq\Pi_5^{\mathds{C}}$.
%\end{lem}
%
%\begin{proof}
%Let $\mathds{B}$ be the restriction of $\mathds{A}$ to $\sigma$. Then, by definition, $\mathds{B}$ should be an encoding expansion $\mathds{A}$. Now we show:
%
%``$\Longrightarrow$": Assume that $M$ is a model of $\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\omega}$.
%As no intensional predicate of $\Pi_5$ appears in the body of any rule in $\Pi_5$, each rule in $\Pi_5^{\mathds{C}}$ should be $\bot$ or a fact, i.e. a ground atom. We first show the first case is not true. Clearly, we have $\bot\not\in\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\omega}$. By Lemma \ref{lem:progress_sim}, the element $c_{\epsilon}^{\mathds{C}}$, which encodes the empty clause $\bot$, is then not in $\cup_{n\ge0}\Delta^n(\mathds{B})$. By definition, $\textsc{true}(c_{\epsilon})$ should be false in $\mathds{C}$, which implies that  $\bot\not\in\Pi_5^{\mathds{C}}$. So, $\Pi_5^{\mathds{C}}$ consists of a set of ground atoms. Let $p\in\Pi_5^{\mathds{C}}$. By definition, there must exist an atom $\vartheta$ of form $P(\bar{z}_P)$ (where $P\in\tau$) % and $\bar{z}_P=z_1\cdots z_{k_P}$
%and an assignment $\alpha$ in $\mathds{C}$ such that $\vartheta[\alpha]=p$ and $\alpha$ satisfies the body of the corresponding rule of form (\ref{eqn:pi5_true2}) in $\mathds{C}$.
%By definition, there exists a positive clause $C\in\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\omega}$ such that $\alpha(x)=[\![C]\!]$. As $\textsc{enc}(y,\lceil\vartheta\rceil,x)$ is satisfied by $\alpha$ in $\mathds{C}$, by definition there exists a subclause $C_0$ of $C$ such that $\alpha(y)=[\![C_0]\!]$ and $C=C_0\vee p$. Since $\alpha$ satisfies $\textsc{false}(y)$ in $\mathds{C}$, by definition $C_0$ should be false in $\textsc{Ins}(\mathds{A},\tau)$, and consequently false in $M$. This means $M\cap C_0=\emptyset$. On the other hand, as $\textsc{true}([\![C]\!])$ is true in $\mathds{C}$, we have $C\in\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\omega}$. By the assumption, $M$ should satisfy $C$, or equivalently $M\cap C\ne\emptyset$. These then imply $p\in M$. Thus, we have $M\supseteq\Pi_5^{\mathds{C}}$.
%
%``$\Longleftarrow$": Assume $M\supseteq\Pi_5^{\mathds{C}}$. Let $C$ be a clause in $\Gamma^{\mathds{A}}_{\Pi}\uparrow_{\omega}$. It suffices to show that $C\cap M\ne\emptyset$. Let $a$ denote $[\![C]\!]$. Then, by Lemma \ref{lem:progress_sim}  and the definition of $\mathds{C}$, $\textsc{true}(a)$ is true in $\mathds{C}$. Suppose $C=C_0\vee p$, where $p$ is an atom and $C_0$ a positive clause. If $C_0\cap\textsc{Ins}(\mathds{A},\tau)\ne\emptyset$, we then have $C\cap\textsc{Ins}(\mathds{A},\tau)\ne\emptyset$. Since $M$ Now, let us assume $C_0\cap M=\emptyset$.
%
%
%there is some atom $q$ among $C_0$ that is in $\textsc{Ins}(\mathds{A},\tau)$, $C$ will be satisfied by $\textsc{Ins}(\mathds{A},\tau)$ immediately. Otherwise, by definition, $\textsc{Ins}(\mathds{C},\tau)$ does not satisfy any atom in $C_0$. Let $b$ denote $[\![C_0]\!]$. We can conclude that $\textsc{false}(b)$ is in $\textsc{Ins}(\mathds{C},\tau)$. It is also clear that there is an assignment $\alpha$ in $\mathds{C}$ such that $\alpha(x)=a$, $\alpha(y)=b$ and $\alpha$ satisfies $\textsc{ext}(x,\lceil p\rceil,y)$. Let $\gamma$ be a rule of form (\ref{eqn:pi5_true2}) such that $\vartheta[\alpha]=p$. Obviously, $\gamma[\alpha]$ is a rule in $\Pi_5^{\mathds{C}}$. According to the assumption, $\textsc{Ins}(\mathds{C},\tau)$ is a model of $\gamma[\alpha]$. By previous conclusions, $p$ should be in $\textsc{Ins}(\mathds{C},\tau)$, which implies that $p\in\textsc{Ins}(\mathds{A},\tau)$ by definition. Thus, $C$ is also satisfied by $\textsc{Ins}(\mathds{A},\tau)$. Due to the arbitrariness of $C$, $\textsc{Ins}(\mathds{A},\tau)$ should be a model of $\Gamma^{\mathds{A}}_{\Pi}\uparrow_{\omega}$. This then completes the proof.
%\end{proof}
%
%With this lemma, we can show the following property.

\begin{lem}\label{lem:infinite_pro} Let $\mathds{A}$ be a structure of $\upsilon(\Pi)$ with a progression expansion $\mathds{C}$. Then $\textsc{Ins}(\mathds{A},\tau)$ is a minimal model of $\Gamma${\small$^{\mathds{A}}_{\Pi}$}$\uparrow_{\omega}$ iff $\textsc{Ins}(\mathds{C},\tau)$ is a minimal model of $\Pi${\small$_5^{\mathds{C}}$}.%\vspace{-.05cm}

%, i.e., $\textsc{Ins}(\mathds{C},\tau)=\Pi_5^{\mathds{C}}$.
\end{lem}

Due to the limit of space, we will omit the proofs of Lemmas \ref{lem:progress_sim} and \ref{lem:infinite_pro} here.
To show Lemma \ref{lem:progress_sim}, it is sufficient to show both $[\![\Gamma${\small$^{\mathds{A}}_{\Pi}$}$\uparrow_{n}]\!]\subseteq\Delta${\small$^{2n}$}$(\mathds{B})$ and $[\![\Gamma${\small$^{\mathds{A}}_{\Pi}$}$\uparrow_{n}]\!]\supseteq\Delta${\small$^{n}$}$(\mathds{B})$, and each of them can be done by an induction. For Lemma \ref{lem:infinite_pro}, roughly speaking, the soundness is assured by the result that every head-cycle-free disjunctive program is equivalent to the normal program obtained by shifting~\cite{BD:94}. Please note that every set of positive clauses is head-cycle-free, and $\Pi_4$ and $\Pi_5$ are designed for the simulation of shifting.
%
%
%\begin{proof}
%``$\Longrightarrow$": Assume that $\textsc{Ins}(\mathds{A},\tau)$ is a minimal model of $\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\omega}$. By Lemma \ref{lem:infinite_a&c}, we have $\textsc{Ins}(\mathds{C},\tau)\supseteq\Pi_5^{\mathds{C}}$. Let $M$ be any proper subset of $\textsc{Ins}(\mathds{C},\tau)$. Then $M$ is also a proper subset of $\textsc{Ins}(\mathds{A},\tau)$ by definition. According to the assumption, $M$ cannot satisfy $\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\omega}$. By Lemma \ref{lem:infinite_a&c} again, $M\not\supseteq\Pi_5^{\mathds{C}}$. Due to the arbitrariness of $M$, we conclude $\textsc{Ins}(\mathds{C},\tau)=\Pi_5^{\mathds{C}}$. This implies that $\textsc{Ins}(\mathds{C},\tau)$ is a minimal model of $\Pi_5^{\mathds{C}}$.
%
%``$\Longleftarrow$": Assume that $\textsc{Ins}(\mathds{C},\tau)$ is a minimal model of $\Pi_5^{\mathds{C}}$. By definition, we then have $\textsc{Ins}(\mathds{C},\tau)=\Pi_5^{\mathds{C}}$. By Lemma \ref{lem:infinite_a&c}, $\textsc{Ins}(\mathds{A},\tau)$ should be a model of $\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\omega}$.
%Let $M$ be any proper subset of $\textsc{Ins}(\mathds{A},\tau)$. As $\textsc{Ins}(\mathds{A},\tau)=\textsc{Ins}(\mathds{C},\tau)$, $M$ is also a proper subset of $\textsc{Ins}(\mathds{C},\tau)$. By Lemma \ref{lem:infinite_a&c} again, $M$ cannot be
%
%\end{proof}
%
%\begin{proof}
%``$\Longrightarrow$": Assume that $\textsc{Ins}(\mathds{A},\tau)$ is a minimal model of $\Gamma^{\mathds{A}}_{\Pi}\uparrow_{\omega}$. We first show that $\textsc{Ins}(\mathds{C},\tau)$ is a model of $\Pi_5^{\mathds{C}}$. By assumption, $\textsc{Ins}(\mathds{A},\tau)$ is a model of $\Gamma^{\mathds{A}}_{\Pi}$. So, we must have that $\bot\not\in\Gamma^{\mathds{A}}_{\Pi}$. By Lemma \ref{lem:progress_sim}, the element $c_{\epsilon}^{\mathds{C}}$, which encodes the empty clause $\bot$, is then not in $\Delta^n(\mathds{A}^{+})$. Equivalently, $\textsc{true}(c_{\epsilon})$ is false in $\mathds{C}$. This means that the rule (\ref{eqn:pi5_true1}) is satisfied by $\mathds{C}$. Let $\gamma$ be any rule of form (\ref{eqn:pi5_true2}) and $\alpha$ an arbitrary assignment in $\mathds{C}$ such that $\alpha$ satisfies the body of $\gamma$ in $\mathds{C}$. By definition, there should exist a clause $C\in\Gamma^{\mathds{A}}_{\Pi}$ such that $\alpha(x)=[\![C]\!]$. As $\textsc{ext}(x,\lceil\vartheta\rceil,y)$ is satisfied by $\alpha$ in $\mathds{C}$, by definition there exists a subclause $C_0$ of $C$ such that $\alpha(y)=[\![C_0]\!]$ and $C=C_0\vee p$. By the assumption that $\alpha$ satisfies $\textsc{false}(y)$ in $\mathds{C}$ and $\Pi_4$, $C_0$ should be false in $\textsc{Ins}(\mathds{C},\tau)$, and consequently false in $\textsc{Ins}(\mathds{A},\tau)$ by definition. On the other hand, we have $\textsc{Ins}(\mathds{A},\tau)\cap C\ne\emptyset$ since $\textsc{Ins}(\mathds{A},\tau)$ satisfies of $C$. From it, we can then conclude that $p\in\textsc{Ins}(\mathds{A},\tau)$, which implies $p\in\textsc{Ins}(\mathds{C},\tau)$ immediately. Therefore, $\textsc{Ins}(\mathds{C},\tau)$ is indeed a model of $\Pi_5^{\mathds{C}}$.
%
%
%Let $\pi$ be the set of intensional proposition constants of $\Pi_5^{\mathds{C}}$. Clearly, each intensional proposition constant of $\Pi^{\mathds{A}}$ is in $\pi$. Next, we want to show that $\textsc{Ins}(\mathds{C},\tau)$ is a $\pi$-minimal model of $\Pi_5^{\mathds{C}}$. Let $M$ be any model of $\Pi_5^{\mathds{C}}$ such that $M\subseteq\textsc{Ins}(\mathds{C},\tau)$ and $M\!-\!\pi=\textsc{Ins}(\mathds{C},\tau)\!-\!\pi$. It suffices to show that $M\cap\pi\supseteq\textsc{Ins}(\mathds{C},\tau)\cap\pi$. We claim that for each atom $p\in\pi\cap\textsc{Ins}(\mathds{A},\tau)$ there exists at least one clause, say $C_p$, in $\Gamma^{\mathds{A}}_{\Pi}\uparrow_{\omega}$ such that $C_p\cap\textsc{Ins}(\mathds{A},\tau)=\{p\}$. Otherwise, %one of the following cases should be true:
%%\begin{enumerate}
%%\item for all clauses $C\in\Gamma^{\mathds{A}}_{\Pi}\uparrow_{\omega}$, $p\not\in C\cap\textsc{Ins}(\mathds{A},\tau)$;
%%\item for all clauses $C\in\Gamma^{\mathds{A}}_{\Pi}\uparrow_{\omega}$, $C\cap\textsc{Ins}(\mathds{A})-\{p\}\ne\emptyset$.
%%\end{enumerate}
%%Let us first assume Case 1. L
%let $N=\textsc{Ins}(\mathds{A},\tau)-\{p\}$; it is obvious that $N$ is also a model of $\Gamma^{\mathds{A}}_{\Pi}\uparrow_{\omega}$, a contradiction. With this claim, for each atom $p\in\pi\cap\textsc{Ins}(\mathds{C},\tau)=\pi\cap\textsc{Ins}(\mathds{A},\tau)$ there should be a rule $\gamma$ of form (\ref{eqn:pi5_true2}) and an assignment $\alpha$ in $\mathds{C}$ such that $\vartheta[\alpha]=p$, $\alpha(x)=[\![C_p]\!]$ and $\mathds{C}\models\textsc{ext}(x,\lceil\vartheta\rceil,y)[\alpha]$. It is clear that $\gamma[\alpha]\in\Pi_5^{\mathds{C}}$. Let $C_0$ be the clause obtained from $C_p$ by removing $p$. By the definition of $C_p$, it is clear that each atom in $C_0$ should be false in $\mathds{A}$ (so it is false in $\mathds{C}$ too). As $\alpha(y)$ encodes $C_0$, the ground atom $\textsc{false}(y)[\alpha]$ should be in $\textsc{Ins}(\mathds{C},\tau)-\pi=M-\pi$. It is also easy to check that $\textsc{true}(x)[\alpha],\textsc{ext}(x,\lceil\vartheta\rceil,y)[\alpha]\in\textsc{Ins}(\mathds{C},\tau)-\pi = M-\pi$. Since $M$ satisfies $\gamma[\alpha]$, we must have $p=\vartheta[\alpha]\in M$. Thus, we can conclude that $M\cap\pi\supseteq\textsc{Ins}(\mathds{C},\tau)\cap\pi$.
%
%``$\Longleftarrow$": Assume that $\textsc{Ins}(\mathds{C},\tau)$ is a minimal model of $\Pi_5^{\mathds{C}}$. We first show that $\textsc{Ins}(\mathds{A},\tau)$ is a model of $\Gamma^{\mathds{A}}_{\Pi}\uparrow_{\omega}$. Let $C$ be an arbitrary clause in $\Gamma^{\mathds{A}}_{\Pi}\uparrow_{\omega}$ and let $a$ denote $[\![C]\!]$. Then, by Lemma \ref{lem:progress_sim}  and the definition of $\mathds{C}$, $\textsc{true}(a)\in\textsc{Ins}(\mathds{C},\tau)$.
%\end{proof}
%
%
%To prove this claim, we need check the validity of decoding, and then show that the shift operation preserves the semantics, which is similar to that of Theorem 4.17 in~\cite{BD:94}. Due to the limit of space, we leave the detailed proof to a full version of this paper.
%
%Due to the limit of space, we only show the direction of ``$\Longrightarrow$". The converse direction can be shown by a similar argument. Assume $\textsc{Ins}(\mathds{A},\tau)$ is a minimal model of $\Gamma^{\mathds{A}}_{\Pi}\uparrow\omega$. We first show that $\textsc{Ins}(\mathds{C},\tau)$ satisfies $\Pi_5$. Let $C$ be a clause in $\textsc{gpc}(\tau,A)$ such that $\langle C\rangle\in\textsc{true}^{\mathds{C}}$. By Proposition \ref{prop:fxp2sm}, it holds that $\textsc{true}(\langle C\rangle)\in\Gamma^{\mathds{C}}_{\Pi_3}\uparrow\omega$. By Claim 1, we then have that $C\in\Gamma^{\mathds{A}}_{\Pi}\uparrow\omega$. According to the assumption, it implies that $\textsc{Ins}(\mathds{A},\tau)$ satisfies $C$, which means that there exists at least one grounded atom $\vartheta$ in $C$ such that $\vartheta$ is true in $\mathds{A}$, and so in $\mathds{C}$. This means that $C$ can not be empty, or equivalently, $\langle C\rangle\neq c^{\mathds{C}}_{\epsilon}$, which implies that the rule (\ref{eqn:pi5_true1}) is satisfied by $\mathds{C}$. Furthermore, for every assignment $\alpha$ that assigns $x$ to $\langle C\rangle$, from the conclusion we can infer that $\alpha$ satisfies the rule (\ref{eqn:pi5_true2}) in $\mathds{C}$. Hence, we have that $\textsc{Ins}(\mathds{C},\tau)$ is a model of $\Pi_5^{\mathds{C}}$.
%
%Next, we show the minimality of $\textsc{Ins}(\mathds{C},\tau)$. Towards a contradiction, we assume that there is a model $\mathds{M}$ of $\Pi_5^{\mathds{C}}$ such that $\mathds{M}\subsetneq\textsc{Ins}(\mathds{C},\tau)$. By the definition of $\Pi_5^{\mathds{C}}$, we must have that $\Pi_5^{\mathds{C}}\subseteq\mathds{M}$. Let $\vartheta$ be an intensional atom of $\Pi$ and $\alpha$ an assignment in $\mathds{C}$ such that $\vartheta[\alpha]$ is in $\textsc{Ins}(\mathds{C},\tau)$ but not in $\mathds{M}$. Then by the definition of first-order GL-reduction, for each pair of elements $a,b\in C$, $\alpha^{xy}_{ab}$ does not satisfy the body of rule (\ref{eqn:pi5_true2}) for $\vartheta$ in $\mathds{C}$ (where $\alpha^{xy}_{ab}$ is the assignment obtained from $\alpha$ by reassigning $x,y$ to $a,b$ respectively). This means, for every clause $C$ in $\Gamma^{\mathds{A}}_{\Pi}\uparrow\omega$, if $C$ contains $\vartheta[\alpha]$, there should be some grounded atom $\vartheta_0\neq\vartheta[\alpha]$ such that $\vartheta_0\in\textsc{Ins}(\mathds{C},\tau)$. Let $\mathds{N}$ be $\textsc{Ins}(\mathds{C},\tau)\setminus\{\vartheta[\alpha]\}$. Then it is clear that $\mathds{N}\models C$ and then $\mathds{N}$ is a model of $\Gamma^{\mathds{A}}_{\Pi}\uparrow\omega$. But this is impossible since $\textsc{Ins}(\mathds{C},\tau)=\textsc{Ins}(\mathds{A},\tau)$ is the minimal model of $\Gamma^{\mathds{A}}_{\Pi}\uparrow\omega$.
%
%``$\Longleftarrow$": Assume $\textsc{Ins}(\mathds{D},\tau)$ is a minimal model of $\Pi^{\mathds{D}}_5$. Let $C$ be any clause in $\Gamma^{\mathds{A}}_{\Pi}\uparrow\omega$.
%
%To show the minimality of $\textsc{Ins}(\mathds{A},\tau)$, assume $\mathds{M}$ is a model of $\Gamma^{\mathds{A}}_{\Pi}\uparrow\omega$ such that $\mathds{M}\subseteq\textsc{Ins}(\mathds{A},\tau)$. We show $\mathds{M}$ is also a model of $\Pi_5^{\mathds{C}}$. Let $\gamma$ be a rule of the form (\ref{eqn:pi5_true2}) and let $\alpha$ be an assignment in $\mathds{C}$. If $\alpha$ satisfies the body of $\gamma$, we want to show $\vartheta[\alpha]\in\mathds{M}$. This is clear because: if $ $
%
%\smallskip
With these lemmas, we can then prove Theorem \ref{thm:tran_infinite}:%\vspace{-.1cm}

\begin{proof}[Proof of Theorem \ref{thm:tran_infinite}]
By the splitting lemma in~\cite{FLLP:09} and the second-order transformation, it suffices to show that $\mathrm{SM}(\Pi)$ is equivalent to the following formula%\vspace{-.1cm}
\begin{equation}\label{eqn:splitting}
\exists\pi[\mathrm{SM}(\Pi_1)\wedge\cdots\wedge\mathrm{SM}(\Pi_5)]%\vspace{-.1cm}
\end{equation}
over infinite structures. Now we prove it as follows.


``$\Longrightarrow$": Let $\mathds{A}$ be an infinite model of $\mathrm{SM}(\Pi)$. Let $\mathds{B}$ be an encoding expansion of $\mathds{A}$. The existence of such an expansion is clearly assured by the infiniteness of $A$. It is easy to check that $\mathds{B}$ is a stable model of both $\Pi_1$ and $\Pi_2$. Let $\mathds{C}$ be the progression expansion of $\mathds{A}$ that is also an expansion of $\mathds{B}$. By Proposition \ref{prop:fxp2sm}, $\textsc{Ins}(\mathds{B},\tau)=\textsc{Ins}(\mathds{A},\tau)$ should be a minimal model of $\Gamma${\small$^{\mathds{A}}_{\Pi}$}$\uparrow_{\omega}$. By Lemma \ref{lem:progress_sim} and definition, $\textsc{Ins}(\mathds{B},\tau)$ is also a minimal model of $\Gamma${\small$^{\mathds{B}}_{\Pi_3}$}$\uparrow_{\omega}$. By Proposition \ref{prop:fxp2sm} again, $\mathds{B}$ is then a stable model of $\Pi_3$, which implies that so is $\mathds{C}$. It is also easy to check that $\mathds{C}$ is a stable model of $\Pi_4$. On the other hand, since $\textsc{Ins}(\mathds{A},\tau)$ is a minimal model of $\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\omega}$, by Lemma \ref{lem:infinite_pro}, $\textsc{Ins}(\mathds{C},\tau)$ should be a minimal model of $\Pi${\small$_5^{\mathds{C}}$}, which means that $\mathds{C}$ is a stable model of $\Pi_5$ by Proposition \ref{prop:fo2prop}. Thus, $\mathds{A}$ is a model of formula (\ref{eqn:splitting}).

``$\Longleftarrow$": Let $\mathds{A}$ be an infinite model of formula (\ref{eqn:splitting}). Then there exists an $\upsilon(\Pi^{\diamond})$-expansion $\mathds{C}$ of $\mathds{A}$ such that $\mathds{C}$ satisfies $\mathrm{SM}(\Pi_i)$ for all $i:1\le i\le 5$. Let $\mathds{B}$ be the restrictions of $\mathds{C}$ to $\sigma$. Then, by a routine check, it is easy to show that $\mathds{B}$ is an encoding expansion of $\mathds{A}$. As $\mathds{C}$ is a stable model of $\Pi_3$, by Proposition \ref{prop:fxp2sm}, $\textsc{Ins}(\mathds{C},\upsilon_3)$ is then a minimal model of $\Gamma${\small$^{\mathds{C}}_{\Pi_3}$}\,$\uparrow_{\omega}\,=\Gamma${\small$^{\mathds{B}}_{\Pi_3}$}\,$\uparrow_{\omega}$. Furthermore, by Lemma \ref{lem:progress_sim} and the conclusion that $\mathds{C}$ satisfies $\mathrm{SM}(\Pi_4)$, we then have that $\mathds{C}$ is a progression expansion of $\mathds{A}$. On the other hand, since $\mathds{C}$ is also a stable model of $\Pi_5$, by Proposition \ref{prop:fo2prop} we can conclude that $\textsc{Ins}(\mathds{C},\tau)$ is a minimal model of $\Pi${\small$_5^{\mathds{C}}$}. Thus, by Lemma \ref{lem:infinite_pro} we immediately have that $\textsc{Ins}(\mathds{A},\tau)$ is a minimal model of $\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\omega}$. By Proposition \ref{prop:fxp2sm}, $\mathds{A}$ is then a stable model of $\Pi$.
%
%
% By equation (\ref{eqn:splitting}), $\mathds{B}$ is a model of the formulas $\mathrm{SM}(\Pi_1)$ and $\mathrm{SM}(\Pi_2)$, which implies that $\textsc{enc}$ is interpreted as an encoding function $\textsl{enc}$ on $A$, $c_{\epsilon}$ and $c_P$ for all predicates $P\in\tau$ are interpreted as elements not in the range of $\textsl{enc}$, predicates $\textsc{mrg},\textsc{in},\textsc{subc},\textsc{equ}$ are interpreted as the corresponding functions or predicates $\textsl{mrg},\textsl{in},\textsl{subc},\textsl{equ}$ related to $\textsl{enc}$ and $c_{\epsilon}^{\mathds{C}}$. By equation (\ref{eqn:splitting}) again, $\mathds{C}$ is a stable model of $\Pi_3$ and $\Pi_4$, and by Proposition \ref{prop:fxp2sm}, $\textsc{Ins}(\mathds{C},\upsilon_3)$ is then a minimal model of $\Gamma^{\mathds{B}}_{\Pi_3}\uparrow\omega$. So, we have $\mathds{C}=\mathds{B}^+$. According to Proposition \ref{prop:fo2prop}, $\textsc{Ins}(\mathds{C},\tau)$ should be a minimal model of $\Pi_5^{\mathds{C}}$ as $\mathds{C}$ is clearly a stable model of $\Pi_5$. Applying Claim 2, we then have that $\textsc{Ins}(\mathds{A},\tau)$ is a minimal model of $\Gamma^{\mathds{A}}_{\Pi}\uparrow\omega$. Thus, by Proposition \ref{prop:fxp2sm}, $\mathds{A}$ should be a stable model of $\Pi$.
\end{proof}%\vspace{-.1cm}


\begin{rem}
Note that, given any finite domain $A$, there is no injective function from $A\times A$ into $A$. Therefore, we can not expect that the above translation works on finite structures.
\end{rem}

%From the above theorem, we then get the following result:

\begin{cor}
$\mathrm{DLP}\simeq_{\mathsf{INF}}\mathrm{NLP}$.
\end{cor}


%\begin{equation}
%\exists F(\forall x\exists!y F(x,y)\wedge\forall y\exists!x F(x,y)\wedge\exists y\forall x\neg F(x,y))
%\end{equation}

Now, let us focus on the relationship between logic programs and second-order logic. The following proposition says that,  over infinite structures, normal programs are more expressive than the existential second-order logic, which then strengthens a result in~\cite{ALZZ:12} where such a separation over arbitrary structures was obtained.

\begin{prop}\label{prop:infinite_nlp2eso}
$\mathrm{NLP}\not\le_{\mathsf{INF}}\Sigma^1_1$.
\end{prop}

To show this, our main idea is to define a property that can be defined by a normal program but not by any existential second-order sentence. The property is defined as follows. Let $\upsilon_{\textsc{r}}$ be the vocabulary consisting of a binary predicate $E$ and two individual constants $s$ and $t$. Let $\textsc{Reach}_{i}$ be the class of infinite $\upsilon_{\textsc{r}}$-structures in each of which there is a finite path from $s$ to $t$ via edges in $E$. Now, we show the result.%\vspace{-.1cm}

\begin{proof}[Proof of Proposition \ref{prop:infinite_nlp2eso}]
First show that $\textsc{Reach}_{i}$ is definable in $\mathrm{NLP}$ over infinite structures.
Let $\Pi$ be the normal program%\vspace{-.05cm}
\begin{equation}
\left\{\,P(s)^{^{}}_{_{}},\,\, P(x)\wedge E(x,y)\rightarrow P(y),\,\, \neg P(t)\rightarrow\bot\,\right\}.%\vspace{-.05cm}
\end{equation}
By a simple check, we can show that the formula $\exists P\mathrm{SM}(\Pi)$ defines the desired property over infinite structures.

Next, we prove that $\textsc{Reach}_{i}$ is undefinable in $\Sigma${\small$^1_1$} over infinite structures. Towards a contradiction, assume that there is a first-order sentence $\varphi$ and a finite set $\tau$ of predicates such that $\exists\tau\varphi$ is in $\Sigma${\small$^1_1$} and defines $\textsc{Reach}_{i}$ over infinite structures. Let $R$ be a binary predicate not in $\tau$. Let $\psi$ denote%\vspace{-.05cm}
\begin{equation}
\begin{aligned}
\forall x\exists y R(x&,y)\wedge\forall x\neg R(x,x)\wedge\\
\forall &x\forall y\forall z[R(x,y)\wedge R(y,z)\rightarrow R(x,z)].
\end{aligned}%\vspace{-.05cm}
\end{equation}
Intuitively, it asserts that the relation $R$ is both transitive and irreflexive, and each element in the domain has a successor w.r.t. this relation. It is obvious that such a relation exists if and only if the domain is infinite. Therefore, the formula $\exists\tau\varphi\wedge\exists R\psi$ defines $\textsc{Reach}_i$ over arbitrary structures.

Moreover, let $\gamma_0(x,y)$ be $x=y$; for all $n>0$ let $\gamma_n(x,y)$ denote $\exists z_n(\gamma_{n-1}(x,z_n)\wedge E(z_n,y))$, where each $\gamma_n(x,y)$ asserts that there is a path of length $n$ from $x$ to $y$. Let $\Lambda$ be the set of sentences $\neg\gamma_n(s,t)$ for all $n\ge 0$. Now we claim:

\smallskip
\noindent{\em Claim.} $\Lambda\cup\{\exists\tau\varphi,\exists R\psi\}$ is satisfiable.
\smallskip

To show this, it suffices to show that the first-order theory $\Lambda\cup\{\varphi,\psi\}$ is satisfiable. Let $\Phi$ be a finite subset of $\Lambda$, and let $n=\max\{m\mid\neg\gamma_m(s,t)\in\Phi\}$. Let $\mathds{A}$ be an infinite model of $\psi$ with vocabulary $\upsilon(\varphi)\cup\upsilon(\psi)$ in which the minimal length of paths from $s$ to $t$ via edge $E$ is an integer $>n$. Then $\mathds{A}$ is clearly a model of $\Phi\cup\{\varphi,\psi\}$. Due to the arbitrariness of $\Phi$, by the compactness we then have the desired claim.

\smallskip
Let $\mathds{A}$ be any model of $\Lambda\cup\{\exists\tau\varphi,\exists R\psi\}$. Then according to $\exists R\psi$, $\mathds{A}$ should be infinite, and by $\Lambda$, there is no path from $s$ to $t$ via $E$ in $\mathds{A}$. However, according to $\exists\tau\varphi$, every infinite model of it should be $s$-to-$t$ reachable, a contradiction. Thus, the property $\textsc{Reach}_i$ is then undefinable in $\Sigma^1_1$ over infinite structures. This completes the proof immediately.
%
%$\Pi_{\psi}$:
%\begin{eqnarray}
%\neg R(x,y)&\rightarrow&S(x,y)\\
%\neg S(x,y)&\rightarrow&R(x,y)\\
%R(x,y)&\rightarrow&D(x)\\
%\neg D(x)&\rightarrow&\bot\\
%R(x,x)&\rightarrow&\bot\\
%R(x,y)\wedge R(y,z)&\rightarrow&R(x,z)
%\end{eqnarray}
\end{proof}%\vspace{-.1cm}

The following separation immediately follows from the proof of Theorem 4.1 in~\cite{EGG:96}. Although their statement refers to arbitrary structures, the proof still works if only infinite structures are focused.

\begin{prop}
$\Sigma^{1}_{2}\not\le_{\mathsf{INF}}\mathrm{DLP}$.
\end{prop}

\section{Finite Structures}

This section will focus on the expressiveness of logic programs over finite structures. We first consider %the translatability from logic programs to several fragments of second-order logic, and that for the converse. These will give us a clear picture about the expressiveness of logic programs.
%
%The translatability from $\mathrm{DLP}$ to $\Sigma^1_2$ is trivially true by the second-order definition of general stable model semantics.
%
the relationship between disjunctive and normal programs. Unfortunately, in the general case, we have the following result:%In the general case, the separation of their expressiveness is turned out to be very difficult due to the following result:

\begin{prop}\label{prop:fin_dlp2nlp}
$\mathrm{DLP}\simeq_{\mathsf{FIN}}\mathrm{NLP}$ iff $\mathrm{NP}=\mathrm{coNP}$.\footnote{A similar result for traditional logic programs under the query equivalence can be obtained by the expressiveness results proved by~\cite{Schl:95,EGM:97}.}
\end{prop}

\begin{proof}
%Let $\Sigma^1_2$ denote the set of sentences of the form $\exists\tau\forall\sigma\varphi$, where $\tau$ and $\sigma$ are finite sets of predicate variables, $\varphi$ is a first-order formula. Let $\mathrm{ESO}$ be the set of sentences of the above form such that $\sigma$ is empty.
By Fagin's Theorem~\cite{Fagin:74} and Stockmeyer's logical characterization of the polynomial hierarchy~\cite{Stoc:77},\footnote{In their characterizations of complexity classes, no function constant of positive arity is allowed. However, this restriction can be removed as functions can be easily simulated by predicates.} we have that $\Sigma^1_2\simeq_{\mathsf{FIN}}\Sigma^1_1$ iff $\Sigma^p_2=\mathrm{NP}$. By a routine complexity theoretical argument, it is also true that $\Sigma^p_2=\mathrm{NP}$ iff $\mathrm{NP}=\mathrm{coNP}$. On the other hand, according to the proof of Theorem 6.3 in~\cite{EGM:97}, or by Proposition \ref{prop:so2dlp} in this section, Leivant's normal form~\cite{Leiv:89} and the definition of $\mathrm{SM}$, we can conclude $\mathrm{DLP}\simeq_{\mathsf{FIN}}\Sigma^1_2$;
by Proposition \ref{prop:nlp2eso} in this section, it holds that $\mathrm{NLP}\simeq_{\mathsf{FIN}}\Sigma^1_1$. Combining these conclusions, we then have the desired proposition.
\end{proof}

This result shows us how difficult it is to separate normal programs from disjunctive programs over finite structures. To know more about the relationship, we will try to prove a weaker separation between these two classes. Before doing this, we need to study the relationship between logic programs and second-order logic. For the class of normal programs, we have the following characterization:

%\begin{prop}
%Let $k\geq 0$. Then for every normal logic program $\Pi$ with intensional predicates of arity $\leq k$ there are a first-order sentence $\varphi$ and a finite set $\tau$ of auxiliary predicates and functions of arity $\leq k$ such that $\textsc{SM}(\Pi)\equiv_{\mathsf{FIN}}\exists\tau\varphi$.
%\end{prop}

\begin{prop}\label{prop:nlp2eso}
$\mathrm{NLP}_n^{\textsc{f}}\simeq_{\mathsf{FIN}}\Sigma_{1,n}^{1\textsc{f}}[\forall^{\ast}]$ for all $n>1$.
\end{prop}

%%% k => n   cardinality of A n => k
%Let $\prec$ be a binary predicate. Let $\varpi$ be the formula
%\begin{equation}
%\forall x(\neg x\prec x)\wedge
%\forall x\forall y\forall z(x\prec y\wedge y\prec z\rightarrow x\prec z).
%\end{equation}
%It is clear that a structure is a model of $\varpi$ if and only if $\prec$ is interpreted as a strict partial order on the domain. Suppose that $\bar{s}=s_1\cdots s_m$ and $\bar{t}=t_1\cdots t_m$ are any two tuples of terms, where $m\ge 0$. Let $\bar{s}\prec\bar{t}$ be short for the formula
%\begin{eqnarray}
%\begin{aligned}
%s_1\prec t_1&\vee (s_1=t_1\wedge s_2\prec t_2)\vee\cdots\\
%&\vee (s_1=t_1\wedge\cdots\wedge s_{n-1}=t_{n-1}\wedge s_m\prec t_m).
%\end{aligned}
%\end{eqnarray}
%Intuitively, this formula asserts that $\bar{s}$ is less than $\bar{t}$ w.r.t. the lexicographic order generated by $\prec$ in a standard way.
%

To prove the above characterization, we have to develop a translation that turns normal programs to first-order sentences. The main idea is to extend the Clark completion by a progression simulation, so it is an improved version of the ordered completion proposed by~\cite{ALZZ:12}. %As we will see, the translation is very simple, and the maximal arity of the auxiliary constants in this translation is only $n$ (this is almostly the exact lower bound), while that in ordered completion is $2n$, where $n$ is the maximal arity of intensional predicates in the original normal program.

Now, we define the translation. Let $\Pi$ be a normal program and $n$ the maximal arity of intensional predicates of $\Pi$. Without loss of generality, assume the head of every rule in $\Pi$ is of form $P(\bar{x})$, where $P$ is a $k$-ary predicate for some $k\ge 0$, and $\bar{x}$ is the tuple of distinct individual variables $x_1,\dots,x_k$. Let $\prec$ be a new binary predicate and $\varpi$ a universal first-order sentence asserting that $\prec$ is a strict partial order. Given two tuple $\bar{s},\bar{t}$ of terms of the same length, let $\bar{s}\prec\bar{t}$ be a quantifier-free formula asserting that $\bar{s}$ is less than $\bar{t}$ w.r.t. the lexicographic order extended from $\prec$ naturally.


%\medskip
%\hspace{-.15cm}\begin{tabular}{p{0.86\columnwidth}p{0.07\columnwidth}}
%  % after \\: \hline or \cline{col1-col2} \cline{col3-col4} ...
%  The head of every rule in $\Pi$ is of the form $P(\bar{x})$, where $P$ is a $k$-ary predicate for some $k\ge 0$, and $\bar{x}$ denotes the tuple of individual variables $x_1,\dots,x_k$.
% & %\vspace{.16cm}\hspace{-.12cm}($\ast$) \\
%\end{tabular}
%\smallskip

Let $\tau$ be the set of intensional predicates of $\Pi$. Let $c$ be the least integer $\ge\log_2|\tau|+n$. Fix $P$ to be a $k$-ary predicate in $\tau$ and let $\lambda=P(x_1,\dots,x_k)$. Suppose $\gamma_1,\dots,\gamma_{l}$ list all the rules in $\Pi$ whose heads are $\lambda$, and suppose $\gamma_i$ is of form%\vspace{-.1cm}
\begin{equation}\label{eqn:nlp2eso_rule}
\zeta^i\wedge\vartheta^i_1\wedge\cdots\wedge\vartheta^i_{m_i}\rightarrow\lambda%\vspace{-.1cm}
\end{equation}
where {\small$\vartheta^i_1,\dots,\vartheta^i_{m_i}$} list all the positive intensional conjuncts in the body of $\gamma_i$, {\small$\zeta^i$} is the conjunction of other conjuncts that occurs in the body of $\gamma_i$, $m_i\geq 0$, and $\bar{y}_i$ is the tuple of all individual variables occurring in $\gamma_i$ but not in $\lambda$.

Next, we let $\varphi_{P}$ denote the conjunction of rules $\gamma_i$
for all $i:1\leq i\leq l$, and let $\psi_{P}$ denote the formula%\vspace{-.12cm}
\begin{equation}\label{eqn:nlp2eso_completion2}
\lambda\rightarrow\bigvee_{i=1}^{l}\exists\bar{y}_i\left[\zeta^i\wedge\bigwedge_{j=1}^{m_i}\left(\vartheta^i_j\wedge \textsc{less}_{\textsc{d}}(\vartheta^i_j,\lambda)\right)\right]%\vspace{-.12cm}
\end{equation}
where, for every intensional atoms $\vartheta$ and $\vartheta_0$, $\mathrm{ord}(\vartheta)$ denotes the tuple $(o${\small$_Q^c$}$(\bar{t}),\cdots,o${\small$_Q^{1}$}$(\bar{t}))$ if $\vartheta$ of form $Q(\bar{t})$, each $o${\small$_Q^s$} is a new function whose arity is the same as that of $Q$, and $\textsc{less}_{\textsc{d}}(\vartheta,\vartheta_0)$ denotes formula $\mathrm{ord}(\vartheta)\prec\mathrm{ord}(\vartheta_0)$.

Define $\varphi_{\Pi}$ as the universal closure of conjunction of the formula $\varpi$ and formulas $\varphi_{P}\wedge\psi_{P}$ for all $P\in\tau$. Let $\sigma$ be the set of functions $o${\small$^s_{Q}$} for all $Q\in\tau$ and $s\hspace{-.02cm}:1\hspace{-.02cm}\le\hspace{-.02cm}s\hspace{-.02cm}\le\hspace{-.02cm}c$. Clearly, $\exists\sigma\varphi_{\Pi}$ is equivalent to a sentence in $\Sigma${\small$^{1{\textsc{f}}}_{1,n}$}$[\forall^{\ast}]$ by introducing Skolem functions if $n>1$. Now we show the soundness: %$\mathrm{SM}(\Pi)\equiv_{\mathsf{FIN}}\exists\sigma\varphi_{\Pi}$, where $\sigma$ is the set of constants occurring in $\varphi_{\Pi}$ but not in $\Pi$.


\begin{lem}\label{lem:finite_nlp2eso}
Given any finite structure $\mathds{A}$ of $\upsilon(\Pi)$ with at least two elements in the domain, $\mathds{A}\models\mathrm{SM}(\Pi)$ iff $\mathds{A}\models\exists\sigma\varphi_{\Pi}$.
\end{lem}


\begin{proof}
%``$\Longrightarrow$": Let $\mathds{A}$ be a finite stable model of $\Pi$ with $|A|\ge 2$. Let $N=|A|$. Without loss of generality, we assume that $A$ is the set of natural numbers less than $N$. Notice that every finite structure with domain size $N$ is isomorphic to a structure with this domain. Given an atom $p\in\Gamma${\small$^{\mathds{A}}_{\Pi}\uparrow_{\omega}$}, let $\hbar(p)$ be the largest number $m$ such that $p\not\in\Gamma${\small$^{\mathds{A}}_{\Pi}\uparrow_m$}. Given any other ground intensional atom $q$, let $\hbar(q)=N^{c}-1$. It is easy to see that the representation of $N^{c}-1$ in the base-$N$ numeral system is $\mathbf{r}=\underline{m\cdots m}$, where $m=N-1$ and the length of $\mathbf{r}$ is $c$. Let $\mathds{B}$ be an $\upsilon(\varphi_{\Pi})$-expansion of $\mathds{A}$ such that:
%\begin{enumerate}
%\item predicate $\prec$ is interpreted as $\{(a,b)\in A\times A\mid a<b\}$;
%\item for each $P\in\tau$ and each $i:1\le i\le c$, function $o^i_P$ is interpreted as a function $g$ such that $g(\bar{a})=d_i$ for all tuples $\bar{a}$ on $A$ of the corresponding length if $\underline{d_c\cdots d_1}$ is the representation of $\hbar(P(\bar{a}))$ in the base-$N$ numeral system.
%\end{enumerate}
%It is not difficult to check that $\mathds{B}$ is indeed a model of $\varphi_{\Pi}$.
%
Due to the limit of space, we only show the right-to-left direction. Let $\mathds{B}$ be a finite model of $\varphi_{\Pi}$. By formula $\varpi$, $\mathds{B}$ must interpret predicate $\prec$ as a strict partial order on $B$. Let $\mathds{A}$ be the restriction of $\mathds{B}$ to $\upsilon(\Pi)$. To show that $\mathds{A}$ is a stable model of $\Pi$, by Proposition \ref{prop:fxp2sm} it suffices to show that $\textsc{Ins}(\mathds{A},\tau)=\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\omega}$. We first claim that $\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{m}\,\subseteq\textsc{Ins}(\mathds{A},\tau)$ for all $m\geq 0$. This can be shown by an induction on $m$. The case of $m=0$ is trivial. Let $m>0$ and assume $\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{m-1}\,\subseteq\textsc{Ins}(\mathds{A},\tau)$. Our task is to show $\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{m}\,\subseteq\textsc{Ins}(\mathds{A},\tau)$. Let $p$ be a ground atom in $\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{m}$. By definition, there must exist a rule $\gamma_i$ of form (\ref{eqn:nlp2eso_rule}) in $\Pi$ and an assignment $\alpha$ in $\mathds{A}$ such that $\lambda[\alpha]=p$, $\alpha$ satisfies $\zeta^i$ in $\mathds{A}$ (so equivalently, in $\mathds{B}$), and for each atom $\vartheta${\small$^i_j$}, $\vartheta${\small$^i_j$}$[\alpha]\in\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{m-1}$. By the inductive assumption, each $\vartheta${\small$^i_j$}$[\alpha]\in\textsc{Ins}(\mathds{A},\tau)$, or in other words, $\alpha$ satisfies each $\vartheta${\small$^i_j$} in $\mathds{A}$ (so equivalently, in $\mathds{B}$). As $\alpha$ clearly satisfies the rule $\gamma_i$ in $\mathds{B}$, we can conclude that $\alpha$ satisfies $\lambda$ in $\mathds{B}$, which implies  $p=\lambda[\alpha]\in\textsc{Ins}(\mathds{B},\tau)=\textsc{Ins}(\mathds{A},\tau)$. So, the claim is true. From it, we have $\Gamma^{\mathds{A}}_{\Pi}\uparrow_{\omega}\subseteq\textsc{Ins}(\mathds{A},\tau)$.

Now, it remains to prove $\textsc{Ins}(\mathds{A},\tau)\subseteq\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\omega}$.
Towards a contradiction, assume this is not true. Then we must have $\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\omega}\,\subsetneq\textsc{Ins}(\mathds{A},\tau)$ by the previous conclusion.
Given two ground intensional atoms $p_1$ and $p_2$ in $\textsc{Ins}(\mathds{A},\tau)$, we define $p_1<p_2$ if $\textsc{less}_{\textsc{d}}(p_1,p_2)$ is true in $\mathds{B}$. Let $p$ be a $<$-minimal atom in $\textsc{Ins}(\mathds{A},\tau)-\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\omega}$ and suppose $p=P(\bar{a})$ for some $P\in\tau$. Let $\alpha$ be an assignment in $\mathds{B}$ such that $\alpha(\bar{x})=\bar{a}$. By definition, $\alpha$ should satisfy $\psi_{P}$ (in which $\lambda[\alpha]=p$) in $\mathds{B}$. So, there exist an integer $i:1\le i\le l$ and an assignment $\alpha_0$ in $\mathds{B}$ such that (i) $\alpha_0(\bar{x})=\bar{a}$, (ii) $\zeta${\small$^i$}$[\alpha_0]$ is true in $\mathds{B}$, and (iii) for all $j$, $q_j\in\textsc{Ins}(\mathds{B},\tau)=\textsc{Ins}(\mathds{A},\tau)$ and $q_j<\lambda[\alpha_0]$, where $q_j$ denotes $\vartheta${\small$^i_j$}$[\alpha_0]$. As $\lambda[\alpha_0]=\lambda[\alpha]=p$ and $p$ is $<$-minimal  in $\textsc{Ins}(\mathds{A},\tau)-\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\omega}$, we can conclude $q_j\in\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\omega}$ for all $j$. According to the definition of $\psi_P$, the rule $\gamma_i$ (of form (\ref{eqn:nlp2eso_rule})) is in $\Pi$, which implies $q_1\wedge\cdots\wedge q_{m_i}\rightarrow p=\gamma_i^+[\alpha_0]\in\Pi^{\mathds{A}}$. By definition, we then have $p\in\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\omega}$, a contradiction. %This completes the proof.
%
%
%Let $p\in\textsc{Ins}(\mathds{A},\tau)$, and let $\ell(p)$ be the number of atoms $q\in\textsc{Ins}(\mathds{A},\tau)$ such that $q<p$. As both $A$ and $\tau$ are finite, $\ell(p)$ is always a natural number. Next, we prove $p\in\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\ell(p)+1}$. Suppose $p=P(\bar{a})$ for some $l$-ary predicate $P\in\tau$. Let $\lambda=P(x_1,\dots,x_l)$, and let $\gamma_1,\dots,\gamma_k$ list all the rules in $\Pi$ whose heads are $\lambda$, where each $\gamma_i$ is of form (\ref{eqn:nlp2eso_rule}). %Since $P$ is intensional, by assumption [A], $n$ should be greater than $0$. Consequently, the corresponding rules (\ref{eqn:nlp2eso_completion1}) and (\ref{eqn:nlp2eso_completion2}) should be conjuncts of $\varphi_{\Pi}$.
%Let $\alpha$ be an assignment in $\mathds{B}$ such that $\lambda[\alpha]=p$. Since $\mathds{B}$ is a model of $\varphi_{\Pi}$, $\alpha$ must satisfy both $\varphi_P$ and $\psi_P$ in $\mathds{B}$. Consequently, $\alpha$ should satisfy $\textsc{drvbl}(\lambda)$; moreover, there must exist a rule $\gamma_i$ among $\gamma_1,\dots,\gamma_k$ and an assignment $\alpha_0$ in $\mathds{B}$ such that $\alpha_0(x_j)=\alpha(x_j)$ for all $j:1\le j\le l$, and $\alpha_0$ satisfies the following formula in $\mathds{B}$:
%\begin{equation}\label{eqn:nlp2eso_proof_formula}
%\zeta^i\wedge\textsc{less}_{\textsc{d}}(\vartheta^i_1,\lambda)\wedge\cdots\wedge\textsc{less}_{\textsc{d}}(\vartheta^i_{m_i},\lambda).
%\end{equation}
%If $\ell(p)=0$, it is obvious that $m_i=0$ must be true. This will imply that $\zeta^i\rightarrow\lambda$ is a rule in $\Pi$. It is also clear that $\zeta^i$ should be satisfied by $\alpha_0$ in $\mathds{A}$. So, we can infer $p=\lambda[\alpha]=\lambda[\alpha_0]\in\Pi${\small$^{\mathds{A}}$}. By definition, we then have $p\in\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_1$. For the case of $\ell(p)>0$, let us assume  $q\in\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\ell(q)+1}$ for all atoms $q$ in $\textsc{Ins}(\mathds{A},\tau)$ such that $\ell(q)<\ell(p)$. To complete the proof, now it remains to show  $p\in\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\ell(p)+1}$. As we just proved, $\alpha_0$ satisfies formula (\ref{eqn:nlp2eso_proof_formula}) in $\mathds{B}$. Let $q_i=\vartheta_i[\alpha_0]$. By definition, we then have $\ell(q_i)<\ell(p)$. By the inductive assumption, $q_i\in\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\ell(q_i)+1}\,\subseteq\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\ell(p)}$.
%It is also clear that $\alpha_0$ satisfies $\zeta^i$ in $\mathds{A}$. This implies that the rule $q_1\wedge\cdots\wedge q_{m_i}\rightarrow p$ is in $\Pi^{\mathds{A}}$. By definition, we then have $p\in\Gamma${\small$^{\mathds{A}}_{\Pi}$}\,$\uparrow_{\ell(p)+1}$.
%
%
%%(Due to the limit of space, we omit the detailed induction here.)
%Therefore, $\textsc{Ins}(\mathds{A},\tau)=\Gamma^{\mathds{A}}_{\Pi}\uparrow\omega$.
\end{proof}

%\begin{rem}
%%Roughly speaking, the translation presented above generalized the Clark completion by a simulation of the progression of logic programs. On the theoretical aspect, this translation is
%The maximal arity of the auxiliary constants in this translation is $n$. By Proposition \ref{prop:nlp2eso}, this will be the exact lower bound if one can show that $\Sigma${\small$_{1,n}^{1\textsc{f}}$}$[\forall^{\ast}]\not\le_{\mathsf{FIN}}\Sigma${\small$_{1,n-1}^{1\textsc{f}}$}$[\forall^{\ast}]$.
%\end{rem}

\begin{rem}
%Roughly speaking, the translation presented above generalized the Clark completion by a simulation of the progression of logic programs. On the theoretical aspect, this translation is
Let $m$ and $n$ be the number and the maximal arity of intensional predicates respectively. The maximal arity of auxiliary constants in our translation is only $n$ (that of the ordered completion in~\cite{ALZZ:12} is $2n$), which is optimal if Conjecture 1\footnote{It implies $\mathrm{ESO}${\small$^{\textsc{f}}_n$}$[\forall^{\ast}]\simeq_{\mathsf{FIN}}\mathrm{ESO}${\small$^{\textsc{f}}_n$}$[\forall^{n}]$, where the latter is the class of sentences in $\mathrm{ESO}${\small$^{\textsc{f}}_n$}$[\forall^{\ast}]$ with at most $n$ individual variables.} in~\cite{DGO:04} is true. Moreover, the number of auxiliary constants in our translation is $m\cdot(\lceil\log_2 m\rceil+n)$, while that of the ordered completion is $m^2$. (Note that $n$ is normally very small.) %These mean that, in our translation, $O()$
\end{rem}

\begin{rem}
Similar to the work in~\cite{ALZZ:12}, we can develop an answer set solver by calling some SMT solver. By the comparison in the above remark, this approach is rather promising. In addition, as a strict partial order is available in almost all the SMT solvers (e.g., built-in arithmetic relations), our translation can be easily optimized.
\end{rem}


Now we are in the position to prove Proposition \ref{prop:nlp2eso}.



\begin{proof}[Proof of Proposition \ref{prop:nlp2eso}]
``$\geq_{\mathsf{FIN}}$": Let $\varphi$ be any sentence in $\Sigma${\small$^{1{\textsc{f}}}_{1,n}$}$[\forall^{\ast}]$. It is obvious that $\varphi$ can be written as an equivalent sentence of form $\exists\tau\forall\bar{x}(\gamma_1\wedge\cdots\wedge\gamma_k)$ for some $k\geq 0$, where each $\gamma_i$ is a disjunction of atoms or negated atoms, and $\tau$ a finite set of functions or predicates of arity $\leq n$. Let $\Pi$ be a logic program consisting of the rule $\tilde{\gamma}_i\rightarrow\bot$ for each $i:1\leq i\leq k$, where $\tilde{\gamma}_i$ is obtained from $\gamma_i$ by substituting $\vartheta$ for each negated atom $\neg\vartheta$, followed by substituting $\neg\vartheta$ for each atom $\vartheta$, and followed by substituting $\wedge$ for $\vee$. It is easy to check that $\exists\tau\mathrm{SM}(\Pi)$ is in $\mathrm{NLP}${\small$_n^{\textsc{f}}$} and equivalent to $\varphi$.

``$\leq_{\mathsf{FIN}}$": Let $\mathcal{C}${\small$^{=1}$} (respectively, $\mathcal{C}${\small$^{>1}$}) be the class of finite structures with exactly one (respectively, at least two) element(s) in the domain. Let $\Pi$ be a normal program and $\tau$ a finite set of predicates and functions such that $\exists\tau\mathrm{SM}(\Pi)$ is in $\mathrm{NLP}${\small$_n^{\textsc{f}}$}. It is trivial to construct a sentence, say $\zeta$, in $\Sigma${\small$^{1{\textsc{f}}}_{1,n}$}$[\forall^{\ast}]$ such that $\exists\tau\mathrm{SM}(\Pi)$ is equivalent to $\zeta$ over $\mathcal{C}^{=1}$. (Please note that, if the domain is a singleton, a first-order logic program will regress to a propositional one.) By Lemma \ref{lem:finite_nlp2eso}, there is also a sentence $\psi$ in $\Sigma${\small$^{1{\textsc{f}}}_{1,n}$}$[\forall^{\ast}]$ such that $\exists\tau\mathrm{SM}(\Pi)$ is equivalent to $\psi$ over $\mathcal{C}${\small$^{>1}$}. Let $\varphi$ be the following sentence:%\vspace{-.1cm}
\begin{equation}
[\exists x\forall y(x=y)\wedge\zeta]\vee[\exists x\exists z(\neg x=z)\wedge\psi].%\vspace{-.1cm}
\end{equation}
Informally, this formula first test whether or not the domain is a singleton. If it is true, let $\zeta$ work; otherwise let $\psi$ work. Thus, it is easy to show that $\exists\tau\mathrm{SM}(\Pi)$ is equivalent to $\varphi$ over finite structures. It is also clear that $\varphi$ can be written to be an equivalent sentence in $\Sigma${\small$^{1{\textsc{f}}}_{1,n}$}$[\forall^{\ast}]$. (Please note that every first-order quantifier can be regarded as a second-order quantifier over a function variable of arity $0$.)
%We first construct a translation from normal programs to first-order sentences over $\mathcal{C}^{=1}$. Given a normal program $\Pi$, we let $\zeta_{\Pi}$ denote the sentence obtained from $\mathrm{SM}(\Pi)$ by removing all first-order quantifiers, followed by substituting $c$ for all individual variables, where $c$ is a new individual constants. By a routine induction on the structure of formula, we can show $\exists c \zeta_{\Pi}\equiv_{\mathcal{C}^{=1}}\mathrm{SM}(\Pi)$.
%
%
%Clearly, $\zeta_{\Pi}$ can be rewritten as an equivalent sentence of form $\forall\tau\vartheta$, where $\tau$ is a finite tuple of predicate variables and $\vartheta$ is quantifier-free. Furthermore, let $\varrho_{\Pi}$ be the conjunction of $\vartheta${\small$^{\top}_X$}$\wedge\vartheta${\small$^{\bot}_X$} for all $X\in\tau$, where, for each $\otimes\in\{\top,\bot\}$, $\vartheta${\small$^{\otimes}_X$} is obtained from $\vartheta$ by substituting $\otimes$ for all atoms of form $X(\bar{t})$. Let $\mathds{A}$ be an $\upsilon(\Pi)$-structure with $|A|=1$. Now, we claim
%
%\medskip
%\noindent{\em Claim. } $\mathds{A}\models\mathrm{SM}(\Pi)$ iff $\mathds{A}\models\exists c\varrho_{\Pi}$.
%\medskip
\end{proof}

%\begin{rem}
%\end{rem}

%Now, we show the statement ($*$) by an induction on $\prec$. Suppose $P_{\bar{a}}$ is in $\textsc{Ins}(\mathds{A},\tau)$ and minimal in the order $\prec$. As $\mathds{B}$ satisfies the universal closure of $\psi_{\lambda}$, there should be a rule $\gamma$ in $\Pi$ whose head is $P(\bar{x})$, and an assignment $\alpha$ in $\mathds{B}$ that $\alpha$ assigns $\bar{x}$ to $\bar{a}$ and that $\alpha$ satisfies $\textsc{drvless}(P(\bar{x}),\vartheta)$ for all intensional atoms positively occurring in the body of $\gamma$. Let $S_{\gamma}$ be the set all intensional atoms positively occurring in the body of $\gamma$. By the definition, it means that $\vartheta[\alpha]\prec P_{\bar{a}}$ for all $\vartheta\in S_{\gamma}$. By the inductive assumption, we then have that $\vartheta[\alpha]\in\textsc{Ins}(\mathds{A},\tau)$ iff $\vartheta[\alpha]\in\Gamma^{\mathds{A}}_{\Pi}\uparrow\omega$ for all $\vartheta\in S_{\gamma}$.
%
%Let us first assume $P_{\bar{a}}\in\textsc{Ins}(\mathds{A},\tau)$. By the formula $\varphi_{\lambda}$, $\mathds{B}$ satisfies $\textsc{drvbl}(P_{\bar{a}})$.
%
%Next, we want to show $\Gamma^{\mathds{A}}_{\Pi}\uparrow\omega\subseteq\textsc{Ins}(\mathds{A},\tau)$. Let $n\geq 0$ and assume for all $0\leq k<n$, $\Gamma^{\mathds{A}}_{\Pi}\uparrow k\subseteq\textsc{Ins}(\mathds{A},\tau)$. It suffices to show $\Gamma^{\mathds{A}}_{\Pi}\uparrow n\subseteq\textsc{Ins}(\mathds{A},\tau)$. Let $P$ be an $m$-ary predicate in $\tau$ for some $m\geq 0$, and $\bar{a}$ an $m$-tuple of element in $A$ such that $P_{\bar{a}}\in\Gamma^{\mathds{A}}_{\Pi}\uparrow n$. By the definition, there must be a rule $\gamma$ of the form \ref{eqn:} and an assignment $\alpha$ in $\mathds{A}$ such that $\lambda[\alpha]=P_{\bar{a}}$, $\vartheta_{i}[\alpha]\in\Gamma^{\mathds{A}}_{\Pi}\uparrow n-1$, and $\alpha$ satisfies $\zeta$ in $\mathds{A}$.



%``$\Longrightarrow$": Assume $\mathds{A}$ is a finite stable model of $\Pi$. By Proposition \ref{prop:fxp2sm}, we have that $\textsc{Ins}(\mathds{A},\tau)=\Gamma^{\mathds{A}}_{\Pi}\uparrow\omega$ as $\Pi$ is normal. Given an intensional grounded atom $\vartheta$ over $A$, let $\kappa(\vartheta)$ be the least integer $n$ that satisfies $\vartheta\in\Gamma^{\mathds{A}}_{\Pi}\uparrow n$ if $\vartheta\in\Gamma^{\mathds{A}}_{\Pi}\uparrow\omega$; otherwise, let $\kappa(\vartheta)$ be the number $|A|^{c}-1$. Now, we then define $\mathds{B}$ to be an $\upsilon(\varphi_{\Pi})$-expansion of $\mathds{A}$, which satisfies
%\begin{enumerate}
%\item the constants $<$ and $\max$ are interpreted as a linear order and the largest element in this order;
%\item given any $P\in\tau$, for all $1\leq i\leq c$, $o^i_P$ are interpreted as $n$-arity functions $h_i$ on $A$ such that $(h_c(\bar{a}),\dots,h_1(\bar{a}))$ encodes the integer $\kappa(P_{\bar{a}})$ in the lexicographic order for each $n$-tuple $\bar{a}$ on $A$, where $n$ is the arity of $P$.
%\end{enumerate}
%Clearly, such a structure always exists. It is a routine work to verify that $\mathds{B}$ is a model of $\varphi_{\Pi}$. We omit it here.
%%\end{proof}

%\begin{cor}\label{cor:nlp2fo}
%Over finite structures, $\mathrm{NLP}^{k}\subseteq\mathrm{ESO}^k_{\textsc{f}}$ for all $k\geq 0$.
%\end{cor}

%\begin{prop}\label{prop:uso2dlp}
%For every $\Sigma^{1}_{2,k}[\Pi^0_2]$-sentence $\varphi$ there is a $\mathrm{DLP}^k$-program $\Pi$ such that $\varphi$ is equivalent to $\exists\tau\mathrm{SM}(\Pi)$, where $\tau$ is a finite set of predicates of arity $\leq k$.
%\end{prop}

%\begin{thm}
%For each integer $k\geq1$, there is a disjunctive logic program $\Pi\in\mathrm{DLP}^k$
%\end{thm}

\begin{rem}
Assuming Conjecture 1 in~\cite{DGO:04}, by the results of~\cite{Gran85}, $\mathrm{NLP}_k^{\textsc{f}}$ then exactly captures the class of languages computable in $O(n^{k})$-time (where $n$ is the size of input) in Nondeterministic Random Access Machines (NRAMs), and whether an extensional database can be expanded to a stable model of a disjunctive program is decidable in $O(n^k)$-time in NRAMs.
\end{rem}

%By Proposition \ref{prop:nlp2eso}, it is easy to show:

By Proposition \ref{prop:nlp2eso} and the fact that auxiliary functions can be simulated by auxiliary predicates in both logic programs and second-order logic, we have the following result:

\begin{cor}
$\mathrm{NLP}\simeq_{\mathsf{FIN}}\Sigma^1_1$.
\end{cor}

\smallskip
Next, let us focus on the translatability from a fragment of second-order logic to disjunctive programs.
For convenience, in the rest of this paper, we fix $\textsc{succ}$ to be a binary predicate, fix $\textsc{first}$ and $\textsc{last}$ to be two unary predicates, and fix $\upsilon_{\textsc{s}}$ to be the set consisting of these predicates. In particular, unless mentioned otherwise, a logic program or a formula is always assumed to contains no predicate in $\upsilon_{\textsc{s}}$.

\smallskip
%Let $A$ be a set and $R$ a binary relation on $A$. Then, for $a,b\in A$, $a$ is called a {\em direct predecessor} of $b$ (equivalently, $b$ is a {\em direct successor}) of $a$ if $(a,b)\in R$; $R$ is called a {\em successor relation} (on $A$) if each $a\in A$ has at most one direct predecessor and one direct successor, and the transitive closure of $R$ is a strict total order on $A$. Based on these definitions,
%
A structure $\mathds{A}$ is called a {\em successor structure} if:
\begin{enumerate}
\item its vocabulary contains all the predicates in $\upsilon_{\textsc{s}}$, and
\item $\textsc{succ}^{\mathds{A}}$ is a binary relation $R$ on $A$ such that the transitive closure of $R$ is a strict total order and for all $a\in A$, both $|\{b\!\mid\!(a,b)\in R\}|\le 1$ and $|\{b\!\mid\!(b,a)\in R\}|\le 1$ hold, and
\item $\textsc{first}^{\mathds{A}}$ (respectively, $\textsc{last}^{\mathds{A}}$) consists of the least element (respectively, the largest element) in $A$ w.r.t. $\textsc{succ}^{\mathds{A}}$.
\end{enumerate}
By this definition, given a successor structure, both the least and largest elements must exist, so it is then finite. Now, we let {\small$\textsf{SUC}$} denote the class of successor structures.
\smallskip

Let $\Sigma${\small$^1_{2,n}$}\hspace{-.02cm}$[\forall^n\exists^{\ast}]$ be the class of sentences in $\Sigma${\small$^1_{2,n}$}\hspace{-.02cm}$[\forall^{\ast}\exists^{\ast}]$ that involve at most $n$ universal quantifiers. Now we can show:

\begin{lem}\label{lem:so2dlp}
$\Sigma^{1}_{2,n}[\forall^n\exists^{\ast}]\leq_{\mathsf{SUC}}\mathrm{DLP}_n$ for all $n>0$.
\end{lem}


\begin{proof} (Sketch)
Let $\exists\tau\forall\sigma\varphi$ be any sentence in $\Sigma^{1}_{2,n}[\forall^n\exists^{\ast}]$ where $\tau,\sigma$ are finite sets of predicates of arities $\leq n$. Without loss of generality, suppose $\varphi=\forall\bar{x}\exists\bar{y}(\vartheta_1\vee\cdots\vee\vartheta_m)$, where $\bar{x}$ is of length $n$; each $\vartheta_i$ is a finite conjunction of literals. Next, we want to construct a disjunctive program which defines the property expressed by the sentence $\exists\tau\forall\sigma\varphi$.

Before constructing the program, we need to define some notations. Let $\bar{u}$ and $\bar{v}$ be any two tuples of individual variables $u_1\cdots u_k$ and $v_1\cdots v_k$ respectively. Let $\textsc{First}(\bar{u})$ denote the conjunction of $\textsc{first}(u_i)$ for all $i:1\le i\le k$, and let $\textsc{Last}(\bar{u})$ denote the conjunction of $\textsc{last}(u_i)$ for all $i:1\le i\le k$. Moreover, let $\textsc{Succ}_i(\bar{u},\bar{v})$ be the formula%\vspace{-.1cm}
\begin{eqnarray}
\left[
\begin{aligned}
&u_1=v_1\wedge\cdots\wedge u_{i-1}=v_{i-1}\\
&\quad\wedge\textsc{succ}(u_{i},v_{i})\wedge\textsc{last}(u_{i+1})\\
&\quad\wedge\textsc{first}(v_{i+1})\wedge\cdots\wedge\textsc{last}(u_{k})\wedge\textsc{first}(v_{k})
\end{aligned}
\right]
\end{eqnarray}

%\vspace{-.1cm}
\noindent for each $i:1\le i\le k$.

Now let us construct the translation. First we define:
\begin{equation*}
\begin{aligned}
\Delta_1\,&=&\!\!\!\!\!\{&\!\!\!\!\!\!&X(\bar{z})\vee X^c(\bar{z})\,\, &\left|\right.&&\!\!\!\!\! X\in\sigma\cup\tau\,&\!\!\!\!\!\!&\left\}\right.,\\
\Delta_2\,&=&\!\!\!\!\!\{&\!\!\!\!\!\!&\textsc{Last}(\bar{x})\wedge D(\bar{x})\rightarrow X^c(\bar{z})\,\, &\left|\right.&&\!\!\!\!\! X\in\sigma&\!\!\!\!\!\!&\left\}\right.,\\
\Delta_3\,&=&\!\!\!\!\!\{&\!\!\!\!\!\!&\textsc{Last}(\bar{x})\wedge D(\bar{x})\rightarrow X(\bar{z})\,\, &\left|\right.&&\!\!\!\!\! X\in\sigma&\!\!\!\!\!\!&\left\}\right.,\\
\Delta_4\,&=&\!\!\!\!\!\left.\right\{&\!\!\!\!\!\!&\textsc{First}(\bar{x})\wedge\vartheta^c_i(\bar{x},\bar{y})\rightarrow D(\bar{x})\,\,&\left|\right.&&\!\!\!\!\!1\le i\le m&\!\!\!\!\!\!&\left\}\right.,\\
\Delta_5\,&=&\!\!\!\!\!\left.\begin{aligned}\mbox{}\\\mbox{}\end{aligned}\right\{&\!\!\!\!\!\!&
\begin{aligned}
\textsc{Succ}_j(\bar{v},\bar{x})&\wedge D(\bar{v})\wedge\\
&\vartheta^c_i(\bar{x},\bar{y})\rightarrow D(\bar{x})
\end{aligned}\,\, &\left|\begin{aligned}\mbox{}\!\\\mbox{}\!\end{aligned}\right.&&\!\!\!\!\!\!\begin{aligned}
1&\le i\le m\\1&\le j\le n\end{aligned}&\!\!\!\!\!\!&\left\}\hspace{0.005in},\begin{aligned}\,\!\!\\\,\!\!\end{aligned}\right.\\
\Delta_6\,&=&\!\!\!\!\!\{&\!\!\!\!\!\!&\textsc{Last}(\bar{x})\wedge
\neg D(\bar{x})\rightarrow\bot\,\,&&&&\!\!\!\!\!\!&\left\}\right.,
\end{aligned}%%\vspace{-.1cm}
\end{equation*}
%
%\begin{eqnarray}
%X(\bar{u})\vee X^c(\bar{u})
%\end{eqnarray} for all predicates $X$ in $\tau$ or in $\sigma$, (ii) the rules%%\vspace{-.12cm}
%\begin{eqnarray}
%\textsc{Last}(\bar{x})\wedge D(\bar{x})&\rightarrow& Y(\bar{u})\\
%\textsc{Last}(\bar{x})\wedge D(\bar{x})&\rightarrow& Y^c(\bar{u})%%\vspace{-.12cm}
%\end{eqnarray}
%for all predicates $Y$ in $\sigma$, (iii) the rules%%\vspace{-.12cm}
%\begin{eqnarray}
%\label{rule:so2dlp_u1}\textsc{First}(\bar{x})\wedge\vartheta^c_j(\bar{x},\bar{y})&\rightarrow& D(\bar{x})\\
%\label{rule:so2dlp_u2}\textsc{Succ}_i(\bar{z},\bar{x})\wedge D(\bar{z})\wedge\vartheta^c_j(\bar{x},\bar{y})&\rightarrow& D(\bar{x})
%\end{eqnarray}%%\vspace{-.55cm}
%for all $i:1\le i\le n$ and all $j:1\le j\le m$, and (iv) the rule
%\begin{eqnarray}
%\textsc{Last}(\bar{z})\wedge
%\neg D(\bar{z})\rightarrow\bot.
%\end{eqnarray}
where, for each $X\in\sigma\cup\tau$, $X^c$ is a new predicate of the same arity; $\vartheta^c_i$ is the formula obtained from $\vartheta_i$ by substituting $X^c$ for $\neg X$ whenever $X\in\sigma\cup\tau$; $D$ is an $n$-ary new predicate.

%Note that, in general, formulas (\ref{rule:so2dlp_u1}) and (\ref{rule:so2dlp_u2}) are not rules defined previously. However, by applying some distributivity-like laws proposed by~\cite{CPV:05}, they can be replaced by an (strongly) equivalent set of rules.

Let $\Pi$ be the union of $\Delta_1,\dots,\Delta_6$ and $\pi$ the set of new predicates introduced in the translation. Clearly, $\exists\pi\mathrm{SM}(\Pi)$ is in $\mathrm{DLP}^n$. By a similar (slightly more complicated) argument to that in Theorem 6.3 of~\cite{EGM:97}, we can show that $\exists\pi\exists\tau\exists\sigma\mathrm{SM}(\Pi)\equiv_{\mathsf{SUC}}\exists\tau\forall\sigma\varphi$. %This completes the proof.
%
%Let $\Pi$ be the union of $\Pi_1$ and $\Pi_2$. By a similar but slightly more complex argument than that in Theorem 6.3 of~\cite{EGM:97}, we can show that $\forall\sigma\varphi\equiv_{\mathsf{FIN}}\exists\varsigma\mathrm{SM}(\Pi)$, where $\varsigma$ is the set of all predicates in $\upsilon(\Pi)$ but not in $\upsilon(\forall\sigma\varphi)$.
%
%``$\Longrightarrow$": Assume that $\mathds{A}$ is a successor structure that satisfies $\forall\sigma\varphi$. Let $\mathds{B}$ be an $\upsilon(\Pi)$-expansion of $\mathds{A}$ that interprets
%\begin{enumerate}
%\item $D$ to be the full $k$-ary relation $A^k$;
%\item $X^{c}$ to be $A^n-X^{\mathds{A}}$ if $X$ is an $n$-ary predicate in $\tau$;
%\item both $Y$ and $Y^c$ to be $A^n$ if $Y$ is an $n$-ary predicate in $\sigma$.
%\end{enumerate}
%Let $\kappa$ be the set of intensional predicates of $\Pi$. To show that $\mathds{A}$ is a stable model of $\Pi$, by Proposition \ref{prop:fo2prop} it suffices to show that $\textsc{Ins}(\mathds{B},\kappa)$ is a minimal model of $\Pi^{\mathds{B}}$. It is easy to check that $\textsc{Ins}(\mathds{B},\kappa)$ is a model of $\Pi^{\mathds{B}}$. Let $M\subseteq\textsc{Ins}(\mathds{B},\kappa)$ and suppose that $M$ is also a model of $\Pi^{\mathds{B}}$. Next, we show that $\textsc{Ins}(\mathds{B},\kappa)\subseteq M$.
%
%
\end{proof}

Next, we show that this result can be generalized to finite structures. To do this, we need a program to define the class of successor structures. Now we define it as follows.

Let $\Pi_{\textsc{s}}$ be the program consisting of the following rules.%\vspace{-.1cm}
\begin{align}
\label{eqn:succ_1}\!\!\neg\underline{\textsc{less}}(x,y)&\rightarrow\textsc{less}(x,y)\\
\label{eqn:succ_2}\!\!\neg\textsc{less}(x,y)&\rightarrow\underline{\textsc{less}}(x,y)\\
\label{eqn:succ_3}\!\!\textsc{less}(x,y)\wedge\textsc{less}(y,z)&\rightarrow\textsc{less}(x,z)\\
\label{eqn:succ_4}\!\!\textsc{less}(x,y)\wedge\textsc{less}(y,x)&\rightarrow\bot\\
%\textsc{less}(x,y)\wedge\textsc{less}(y,x)\wedge\neg x=y&\rightarrow\bot\\
\label{eqn:succ_5}\!\!\neg\textsc{less}(x,y)\wedge\neg\textsc{less}(y,x)\wedge\neg x=y&\rightarrow\bot\\
\label{eqn:succ_6}\!\!\textsc{less}(x,y)&\rightarrow\underline{\textsc{first}}(y)\\
\label{eqn:succ_7}\!\!\neg\underline{\textsc{first}}(x)&\rightarrow\textsc{first}(x)\\
%\textsc{first}(x)&\rightarrow\textsc{exist\text{-}f}\\
%\neg\textsc{exist\text{-}f}&\rightarrow\textsc{exist\text{-}f}\\
\label{eqn:succ_8}\!\!\textsc{less}(x,y)&\rightarrow\underline{\textsc{last}}(x)\\
\label{eqn:succ_9}\!\!\neg\underline{\textsc{last}}(x)&\rightarrow\textsc{last}(x)\\
\label{eqn:succ_10}\textsc{less}(x,y)\wedge\textsc{less}(y,z)&\rightarrow\underline{\textsc{succ}}(x,z)\\
\label{eqn:succ_11}\neg\underline{\textsc{succ}}(x,y)\wedge\textsc{less}(x,y)&\rightarrow\textsc{succ}(x,y)%\vspace{-.1cm}
\end{align}
Informally, rules (\ref{eqn:succ_1})--(\ref{eqn:succ_2}) are choice rules to guess a binary relation $\textsc{less}$; rule (\ref{eqn:succ_3}), (\ref{eqn:succ_4}) and (\ref{eqn:succ_5}) restrict $\textsc{less}$ to be transitive, antisymmetric and total respectively so that it is a strict total order; rules (\ref{eqn:succ_6})--(\ref{eqn:succ_7}) and rules assert that $\textsc{first}$ and $\textsc{last}$ consist of the least and the last elements respectively if they exist; the last two rules then assert that $\textsc{succ}$ defines the relation for direct successors.
The following simple lemma shows that $\Pi_{\textsc{s}}$ is the desired program.

%\begin{lem}
%Given a vocabulary $\sigma\supseteq\upsilon_{\textsc{s}}$,
%a $\sigma$-structure $\mathds{A}$ is a stable model of $\Pi_{\textsc{o}}$ if and only if it is an ordered structure.
%\end{lem}

\begin{lem}\label{lem:successor}
Given a vocabulary $\sigma\supseteq\upsilon_{\textsc{s}}$ and a structure $\mathds{A}$ of $\sigma$, $\mathds{A}$ is a successor structure iff it is finite and is a model of $\exists\tau\mathrm{SM}(\Pi_{\textsc{s}})$, where $\tau$ denotes  $\upsilon(\Pi_{\textsc{s}})-\upsilon_{\textsc{s}}$.
\end{lem}

%\begin{proof}
%By Proposition \ref{prop:fo2prop} and a routine check.
%\end{proof}

Now we can then prove the following result:

\begin{prop}\label{prop:so2dlp}
$\Sigma^{1}_{2,n}[\forall^n\exists^{\ast}]\leq_{\mathsf{FIN}}\mathrm{DLP}_n$ for all $n>1$.
\end{prop}


%\begin{prop}\label{prop:so2dlp}
%Let $\Sigma$ and $\Lambda$ be two sets of second-order sentences such that $\Lambda$ is closed under conjunction and contains $\exists\sigma_{\textsc{s}}\mathrm{SM}(\Pi_{\textsc{s}})$. Then $\Sigma\leq_{\mathsf{FIN}}\Lambda$ if and only if $\Sigma\leq_{\mathsf{SUC}}\Lambda$.
%\end{prop}

\begin{proof}
Let $n>1$ and $\varphi$ a sentence in $\Sigma^{1}_{2,n}[\forall^n\exists^{\ast}]$. Let $\Pi_0$ be the disjunctive program constructed in the proof of Lemma \ref{lem:so2dlp} related to $\varphi$, and let $\sigma$ be the set of predicates appearing in $\Pi_0$ but neither in $\upsilon_{\textsc{s}}$ nor in $\upsilon(\varphi)$. Let $\Pi=\Pi_0\cup\Pi_{\textsc{s}}$ and let $\tau$ be the set of predicates appearing in $\Pi_{\textsc{s}}$ but not in $\upsilon_{\textsc{s}}$.
Next we show that $\varphi$ is equivalent to
$\exists\tau\exists\sigma\mathrm{SM}(\Pi)$ over finite structures. By definition and the splitting lemma in~\cite{FLLP:09}, it suffices to show that $\varphi$ is equivalent to%\vspace{-.1cm}
\begin{equation}\label{eqn:dlp2so_fin_formula}
\exists\upsilon_{\textsc{s}}(\exists\tau\mathrm{SM}(\Pi_{\textsc{s}})\wedge\exists\sigma\mathrm{SM}(\Pi_{0}))%\vspace{-.1cm}
\end{equation}
over finite structures. Let $\upsilon$ denote the union of $\upsilon(\varphi)$ and $\upsilon_{\textsc{s}}$. Now we prove the new statement as follows.

``$\Longrightarrow$": Let $\mathds{A}$ be a finite model of $\varphi$. Clearly, there must exist at least one $\upsilon$-expansion, say $\mathds{B}$, of $\mathds{A}$ such that $\mathds{B}$ is a successor structure. By Lemma \ref{lem:successor}, $\mathds{B}$ should be a model of $\exists\tau\mathrm{SM}(\Pi_{\textsc{s}})$, and by the proof of Lemma \ref{lem:so2dlp}, $\mathds{B}$ is also a model of $\exists\sigma\mathrm{SM}(\Pi_0)$. Hence, $\mathds{A}$ is a model of formula (\ref{eqn:dlp2so_fin_formula}).

``$\Longleftarrow$": Let $\mathds{A}$ be a finite model of formula (\ref{eqn:dlp2so_fin_formula}). Then there is an $\upsilon$-expansion, say $\mathds{B}$, of $\mathds{A}$ such that $\mathds{B}$ satisfies both $\exists\tau\mathrm{SM}(\Pi_{\textsc{s}})$ and $\exists\sigma\mathrm{SM}(\Pi_0)$. By Lemma \ref{lem:successor}, $\mathds{B}$ is a successor structure, and then by the proof of Lemma \ref{lem:so2dlp}, $\mathds{B}$ must be a model of $\varphi$. This means that $\mathds{A}$ is a model of $\varphi$.
\end{proof}

%\begin{cor}\label{prop:so2dlp}
%$\Sigma^{1}_{2,n}[\forall^n\exists^{\ast}]\leq_{\mathsf{FIN}}\mathrm{DLP}^n$ for all $n>1$.
%\end{cor}


With these results, we can prove a weaker separation:

\begin{thm}
$\mathrm{DLP}_{n}\not\leq_{\mathsf{FIN}}\mathrm{NLP}_{2n-1}^{\textsc{f}}$ for all $n>1$.
\end{thm}
%
%\begin{lem}
%$\mathrm{DLP}^{k}\not\leq_{\mathsf{SUC}}\mathrm{NLP}^{2k-1}_{\textsc{f}}$ for all $k>0$.
%\end{lem}

\begin{proof}
%(Sketch)
Let $\upsilon_n$ be the vocabulary consisting of only an $n$-ary predicate $P_n$. Define $\textsc{Parity}^n$ to be the class of finite $\upsilon_n$-structures in each of which $P_n$ is interpreted as a set consisting of an even number of $n$-tuples. Fix $n>1$. Now, let us show that $\textsc{Parity}${\small$^{2n}$} is definable in $\mathrm{DLP}_n$ over $\mathsf{FIN}$.

We first show that, over successor structures, $\textsc{Parity}${\small$^{2n}$} is definable in $\Sigma${\small$^1_{2,n}$}$[\forall^{n}\exists^{\ast}]$. Let $\textsc{First},\textsc{Last}$ and $\textsc{Succ}_i$ be the same as those in the proof of Lemma \ref{lem:so2dlp}, and let $\textsc{Succ}(\bar{s},\bar{t})$ denote the conjunction of $\textsc{Succ}_i(\bar{s},\bar{t})$ for all $i\!:\!1\le i\le n$ if $\bar{s}$ and $\bar{t}$ are $n$-tuples of terms. Let $X$ and $Y$ be two predicate variables of arity $n$.
We define $\varphi_1$ to be the formula%%\vspace{-.1cm}
\begin{equation*}
\begin{aligned}
\left[\begin{aligned}
&\forall\bar{z}(\textsc{First}(\bar{z})\rightarrow[Y(\bar{z})\leftrightarrow\,P_{2n}(\bar{x},\bar{z})])\wedge\\
&\forall\bar{y}\bar{z}(\textsc{Succ}(\bar{y},\bar{z})\rightarrow
[P_{2n}(\bar{x},\bar{z})\leftrightarrow Y(\bar{y})\oplus Y(\bar{z})])
\end{aligned}\right]\qquad\\
\rightarrow\exists\bar{z}(\textsc{Last}(\bar{z})\wedge[X(\bar{x})\leftrightarrow Y(\bar{z})]),
\end{aligned}%%\vspace{-.1cm}
\end{equation*}
where $\psi\oplus\chi$ denotes the formula $(\psi\leftrightarrow\neg\chi)$. Informally, $\varphi_1$ is intended to define ``$X(\bar{a})$ is true if and only if the cardinality of $\{\bar{b}\mid P(\bar{a},\bar{b})\}$ is odd". Define $\varphi_2$ to be the formula%%\vspace{-.1cm}
\begin{equation*}
\begin{aligned}
\left[\begin{aligned}
&\forall\bar{z}(\textsc{First}(\bar{z})\rightarrow[X(\bar{z})\leftrightarrow\,Y(\bar{z})])\wedge\\
&\forall\bar{y}\bar{z}(\textsc{Succ}(\bar{y},\bar{z})\rightarrow[X(\bar{z})\leftrightarrow Y(\bar{y})\oplus Y(\bar{z})])
\end{aligned}\right]\qquad\\
\rightarrow\exists\bar{z}[\textsc{Last}(\bar{z})\wedge\neg Y(\bar{z})].
\end{aligned}%%\vspace{-.1cm}
\end{equation*}
Intuitively, $\varphi_2$ asserts ``$X$ consists of an even number of $n$-tuples on the domain". Now, let $\varphi=\exists X\forall Y\forall\bar{x}(\varphi_1\wedge\varphi_2)$. Obviously, $\varphi$ can be written as an equivalent sentence in $\Sigma${\small$^1_{2,n}$}$[\forall^{n}\exists^{\ast}]$. By a careful check,
it is not difficult to show that, given any successor structure $\mathds{A}$ of $\upsilon(\varphi)$, the restriction of $\mathds{A}$ to $\upsilon${\small$_{2n}$} is in $\textsc{Parity}${\small$^{2n}$} if and only if $\mathds{A}$ is a model of $\varphi$.

According to the proof of Lemma \ref{lem:so2dlp}, there exist a disjunctive program $\Pi_{0}$ and a finite set $\tau$ of predicates of arities $\le n$ such that $\exists\tau\mathrm{SM}(\Pi_0)$ is equivalent to $\varphi$ over successor structures and no predicate in $\upsilon_{\textsc{s}}$ is intensional w.r.t. $\Pi_0$. Let $\Pi$ be the union of $\Pi_{\textsc{s}}$ and $\Pi_{0}$. Let $\sigma$ be the set of predicates in $\upsilon(\Pi)-\upsilon${\small$_{2n}$}. It is easy to show that, over finite structures, $\textsc{Parity}${\small$^{2n}$} is defined by $\exists\sigma\mathrm{SM}(\Pi)$, so definable in $\mathrm{DLP}_n$.

Next, we show that $\textsc{Parity}${\small$^{2n}$} is undefinable in $\mathrm{NLP}${\small$_{2n-1}^{\textsc{f}}$} over finite structures. If this is true, we then obtain the desired proposition immediately.
By Proposition \ref{prop:nlp2eso}, it is sufficient to prove that $\textsc{Parity}${\small$^{2n}$} is not definable in $\Sigma${\small$_{1,2n-1}^{1\textsc{f}}$} over finite structures. Towards a contradiction, assume that it is not true. By a similar argument to that in Theorem 3.1 of~\cite{DLS:98}, we have:

\medskip
\noindent{\em Claim}. Let $m\ge\!1$. Then $\textsc{Parity}${\small$^{2m}$} is definable in $\Sigma${\small$_{1,2m-2}^{1\textsc{f}}$} over $\mathsf{FIN}$ if $\textsc{Parity}${\small$^{m}$} is definable in $\Sigma${\small$_{1,m-1}^{1\textsc{f}}$} over $\mathsf{FIN}$. %Every $\upsilon${\small$_{4n}$}-structure $\mathds{A}$ is in $\textsc{Parity}^{4n}$ iff $\mathds{A}\models\psi^{\textsc{t}}$.
\medskip

With this claim, we can then infer that $\textsc{Parity}${\small$^{4n}$} is definable in $\Sigma${\small$_{1,4n-2}^{1\textsc{f}}$} over finite structures. As every function variable of arity $k\ge 0$ can always be simulated by a predicate variable of arity $k+1$, $\textsc{Parity}${\small$^{4n}$} should be definable in $\Sigma${\small$_{1,4n-1}^{1}$} over finite structures, which contradicts with Theorem 2.1 in~\cite{Ajtai:83}. This completes the proof.% So, to complete the proof, it suffices to show the following claim.
%
%
%\medskip
%\noindent{\em Claim} 1. Let $m\ge\!1$. Then $\textsc{Parity}${\small$^{2m}$} is definable in $\Sigma${\small$_{1,2m-2}^{1\textsc{f}}$} over $\mathsf{FIN}$ if $\textsc{Parity}${\small$^{m}$} is definable in $\Sigma${\small$_{1,m-1}^{1\textsc{f}}$} over $\mathsf{FIN}$. %Every $\upsilon${\small$_{4n}$}-structure $\mathds{A}$ is in $\textsc{Parity}^{4n}$ iff $\mathds{A}\models\psi^{\textsc{t}}$.
%\medskip
%
%
%It is clear that every sentence in $\Sigma${\small$_{1,2n-1}^{1\textsc{f}}$} is equivalent to a sentence in the same class without involving predicate variables. This is because that predicate variables can be simulated by function variables of the same arities. Therefore, in the rest of this proof, we do not consider formulas with predicate variable. Given any formula $\psi$ of $\upsilon${\small$_{2n}$}, we then define
%$\psi^{\textsc{t}}$ to be the formula obtained from $\psi$ by
%\begin{enumerate}
%\item substituting predicate $P${\small$_{4n}$} for $P${\small$_{2n}$}, and followed by
%\item substituting expression $``g^{\ast}(\bar{t}),g^{\star}(\bar{t})"$ for each term $g(\bar{t})$ whenever $g$ is a function variable, and followed by
%\item substituting the quantifiers $\exists g^{\ast}\exists g^{\star}$ for each quantifier $\exists g$,
%\end{enumerate}
%where, if $g$ is of arity $k$, then $g^{\ast}$ and $g^{\star}$ are two distinct function variables of arity $2k$ that have never be used.
%
%For example, let $\zeta$ be the formula $\exists g\forall x P_2(x,g(x))$. Then, by definition $\zeta^{\textsc{t}}$ is the following formula (note that individual variables are regarded as nullary function variables):
%\begin{equation}
%\exists g^{\ast}\exists g^{\star}\forall x^{\ast}\forall x^{\star} P_4(x^{\ast},x^{\star},g^{\ast}(x^{\ast},x^{\star}),g^{\star}(x^{\ast},x^{\star})).
%\end{equation}
%
%
%Let $\psi$ be an arbitrary sentence in $\Sigma${\footnotesize$_{1,2n-1}^{1\textsc{f}}$}. By definition, it is clear that $\psi^{\textsc{t}}$ is a sentence in $\Sigma${\footnotesize$_{1,4n-2}^{1\textsc{f}}$}. Now we claim:
%
%\medskip
%\noindent{\em Claim} 1. If $\psi$ defines $\textsc{Parity}^{2n}$\!, $\psi^{\textsc{t}}$ then defines $\textsc{Parity}^{4n}$\!. %Every $\upsilon${\small$_{4n}$}-structure $\mathds{A}$ is in $\textsc{Parity}^{4n}$ iff $\mathds{A}\models\psi^{\textsc{t}}$.
%\medskip
%
%%First suppose this claim is true and, towards a contradiction, assume it is true. Towards a contradiction,
%
%%By Claim  similar to that in Theorem 3.1 of~\cite{DLS:98}, we can then construct a formula $\psi_0$ in $\mathrm{ESO}^{4k-2}_{\textsc{f}}$ to define $\textsc{Parity}^{4k}$. However, according to Theorem 2.1 of~\cite{Ajtai:83}, this is impossible since $\psi_0$ has an equivalent in $\mathrm{ESO}^{4k-1}$, i.e., the set of formulas in $\mathrm{ESO}^{4k-1}_{\textsc{f}}$ without function variables. This then completes the proof.
%
%To show this claim, we still need to define some notations and show another claim.
%%Given a formula
%%
%%$P(x_1,x_2,\dots,x_m)\Longrightarrow P^{\textsc{t}}(x_1^1,x_1^2,x_2^1,x_2^2,\dots,x_m^1,x_m^2)$
%%
%%$f(x_1,x_2,\dots,x_m)\Longrightarrow f^{\textsc{t}}_1(x_1^1,x_1^2,x_2^1,x_2^2,\dots,x_m^1,x_m^2)$
%Let $\mathds{A}$ be any structure of $\upsilon${\small$_{4n}$}. We then define $\mathds{A}^{\textsc{e}}$ to be the structure of $\upsilon${\small$_{2n}$} such that:
%\begin{enumerate}
%\item the domain of $\mathds{A}^{\textsc{e}}$ is $A\times A$;
%\item the $2n$-tuple $((a_1,a_2),\dots,(a_{4n-1},a_{4n}))$ is in $P${\small$_{2n}^{\mathds{A}^{\textsc{e}}}$} if and only if the $4n$-tuple $(a_1,\dots,a_{4n})$ is in $P${\small$_{4n}^{\mathds{A}}$}.
%\end{enumerate}
%Furthermore, let $\alpha$ be any assignment in $\mathds{A}$, and define $\alpha^{\textsc{e}}$ to be an assignment in $\mathds{A}^{\textsc{e}}$ such that:
%\begin{equation}
%\begin{aligned}
%\alpha^{\textsc{e}}(g)((a_1&,a_2),\dots,(a_{2k-1},a_{2k}))=\\
%(&\alpha(g^{\ast})(a_1,\dots,a_{2n}),\alpha(g^{\star})(a_1,\dots,a_{2n})).
%\end{aligned}
%\end{equation}
%for all $k$-ary function variable $g$ appearing in $\psi$ and all elements $a_1,\dots,a_{2k}\in A$. Let $\vartheta$ be any subformula of $\psi$. By a routine induction on the structure of $\vartheta$, we can show:
%%
%%
%%On the other hand, given a second-order sentence $\varphi$ of $\upsilon_n$, let $\varphi^{\textsc{t}}$ be the second-order sentence obtained from $\varphi$ by
%%\begin{enumerate}
%%\item substituting predicate $P${\small$_{2n}$} for $P_{n}$, and followed by
%%\item substituting expression ``$g_{\ast}(\bar{t}),g_{\star}(\bar{t})$" for each term $g(\bar{t})$ whenever $g$ is a normal function variable, and followed by
%%\item substituting the quantifiers $\exists g_{\ast}\exists g_{\star}$ for each quantifier $\exists g$.
%%\end{enumerate}
%%
%%For example, let $\varphi$ be the formula $\exists g\forall x P_2(x,g(x))$. Then $\varphi^{\textsc{t}}$ is defined to be the following formula (note that individual variables are regarded as nullary function variables):
%%\begin{equation}
%%\exists g_{\ast}\exists g_{\star}\forall x_{\ast}\forall x_{\star} P_4(x_{\ast},x_{\star},g_{\ast}(x_{\ast},x_{\star}),g_{\star}(x_{\ast},x_{\star})).
%%\end{equation}
%
%
%\medskip
%\noindent{\em Claim} 2. $\mathds{A}^{\textsc{e}}\models\vartheta[\alpha^{\textsc{e}}]$ iff $\mathds{A}\models\vartheta^{\textsc{t}}[\alpha]$.
%\medskip
%
%
%%This claim can be proved . With it, we can show the following property.
%%
%%\medskip
%%\noindent{\em Claim} 2. Let $n\ge 1$ be an integer. If $\textsc{Parity}^{n}$ is defined by $\varphi$, then $\textsc{Parity}^{2n}$ is defined by $\varphi^{\textsc{t}}$.
%%\medskip
%
%Now we show Claim 1. Assume that $\psi$ defines $\textsc{Parity}${\small$^{2n}$} over finite structures. Let $\mathds{A}$ be an arbitrary structure of $\upsilon${\small$_{4n}$}. Then $\mathds{A}$ is in $\textsc{Parity}${\small$^{4n}$} if and only if (by definition) $\mathds{A}^{\textsc{e}}$ is in $\textsc{Parity}${\small$^{2n}$}, if and only if (by the assumption)  $\mathds{A}^{\textsc{e}}$ satisfies $\psi$, if and only if (by Claim 2) $\mathds{A}$ satisfies $\psi^{\textsc{t}}$. So, $\psi^{\textsc{t}}$ defines $\textsc{Parity}^{2n}$ over finite structures, and then Claim 1 holds.
\end{proof}%%\vspace{-.4cm}


%Let $\mathcal{C}$ be a class of structures. $\varphi$ defines $\mathcal{C}$


%\begin{cor}
%intranslatabilit
%\end{cor}

\section{Arbitrary Structures}

Based on the results presented in the previous two sections, we can then compare the expressiveness of disjunctive programs and normal programs over arbitrary structures.

%in this section, we show that the translatability from disjunctive logic programs to normal logic programs over arbitrary structures is the same as that over finite structures, so equivalent to the question whether $\mathrm{NP}$ is closed under complement.

\begin{thm}\label{thm:arb_dlp2nlp}
$\mathrm{DLP}\simeq\mathrm{NLP}$ iff $\mathrm{DLP}\simeq_{\mathsf{FIN}}\mathrm{NLP}$.
\end{thm}

\begin{proof} %(Sketch)
The left-to-right direction is trivial. Now let us show the converse. Assume $\mathrm{DLP}\simeq_{\mathsf{FIN}}\mathrm{NLP}$, and let $\Pi$ be a disjunctive program. Then there must exist a normal program $\Pi^{\circ}$ such that $\mathrm{SM}(\Pi)\equiv_{\mathsf{FIN}}\exists\sigma\mathrm{SM}(\Pi^{\circ})$, where $\sigma$ is the set of predicates occurring in $\Pi^{\circ}$ but not in $\Pi$. By Theorem \ref{thm:tran_infinite}, there is a normal program $\Pi^{\diamond}$ such that $\mathrm{SM}(\Pi)\equiv_{\mathsf{INF}}\exists\tau\mathrm{SM}(\Pi^{\diamond})$. Without loss of generality, let us assume  $\sigma\cap\tau=\emptyset$. To show $\mathrm{DLP}\simeq\mathrm{NLP}$, our idea is to design a normal program testing whether or not the intended structure is finite. If that is true, we let $\Pi^{\circ}$ work; otherwise, let $\Pi^{\diamond}$ work. To do this, we introduce a new predicate $\textsc{finite}$ of arity 0, and let
%\begin{eqnarray}
%\forall xyz[R(x,y)\wedge R(y,z)\rightarrow R(x,z)]\\
%\forall x\exists y R(x,y)\\
%\forall x\neg R(x,x)
%\end{eqnarray}
%
$\Pi_{\textsc{t}}$ be the union of $\Pi_{\textsc{s}}$ and the following logic program: %\vspace{-.1cm} %$\Pi_{\textsc{f}}$:%%\vspace{-.1cm}
\begin{equation}
\left\{\qquad\begin{aligned}
\textsc{first}(x)&\rightarrow\textsc{num}(x),\\
\textsc{num}(x)\wedge\textsc{succ}(x,y)&\rightarrow\textsc{num}(y),\\
\textsc{num}(x)\wedge\textsc{last}(x)&\rightarrow\textsc{finite}
%\neg\textsc{finite}&\rightarrow\textsc{infinite}
\end{aligned}\qquad\right\}.%\vspace{-.1cm}
\end{equation}
Let $\pi=\upsilon(\Pi_{\textsc{t}})-\{\textsc{finite}\}$. We then have the following:

\smallskip
\noindent{\em Claim.} If $\mathds{A}\models\!\exists\pi\mathrm{SM}(\Pi_{\textsc{t}})$, then $\mathds{A}$ is finite iff $\mathds{A}\models\textsc{finite}$.
\smallskip

The left-to-right direction follows from Lemma \ref{lem:successor}. We only show the converse. Let us assume that $\mathds{A}$ satisfies both $\textsc{finite}$ and $\exists\pi\mathrm{SM}(\Pi_{\textsc{t}})$. Let $\upsilon_0$ be the union of $\upsilon(\Pi_{\textsc{t}})$ and the vocabulary of $\mathds{A}$. Then, there must exist an $\upsilon_0$-expansion $\mathds{B}$ of $\mathds{A}$ such that $\mathds{B}$ is a stable model of $\Pi_{\textsc{t}}$. So, $\textsc{less}^{\mathds{B}}$ should be a strict total order on $A$; the element in $\textsc{first}^{\mathds{B}}$ (respectively, $\textsc{last}^{\mathds{B}}$), if it exists, should be the least (respectively, largest) element in $A$ w.r.t. $\textsc{less}^{\mathds{B}}$; and $\textsc{succ}^{\mathds{B}}$ should be the relation defining the direct successors w.r.t. $\textsc{less}^{\mathds{B}}$. As $\textsc{finite}$ is true in $\mathds{A}$, there must exist an integer $n\ge0$ and $n$ elements $a_1,\dots,a_n$ in $A$ such that $\textsc{first}(a_1),\textsc{last}(a_n)$ and each $\textsc{succ}(a_i,a_{i+1})$ are true in $\mathds{B}$. We assert that every element in $A$ should be $a_i$ for some $i$. If not, let $b$ be one of such elements. As $\textsc{less}^{\mathds{B}}$ is a strict total order, there must exist $i\hspace{-.03cm}:\hspace{-.03cm}1\hspace{-.03cm}\le\hspace{-.03cm}i\hspace{-.03cm}<\hspace{-.03cm}n$ such that both $\textsc{less}(a_i,b)$ and $\textsc{less}(b,a_{i+1})$ are true in $\mathds{B}$. But this is impossible since $\textsc{succ}(a_i,a_{i+1})$ is true in ${\mathds{B}}$. So, we must have $A=\{a_1,\dots,a_n\}$. This implies that $\mathds{A}$ is finite, and then we obtain the claim.

\smallskip
%and rule $\textsc{arc}(x,y)\wedge\textsc{arc}(y,z)\rightarrow\textsc{arc}(x,z)$.
%This program sets flag $\textsc{inf}$ to be true if the intended model is infinite.
%When the intended model is finite, we use program $\Pi_{\mathrm{fin}}$ to set flag $\textsc{fin}$, which is obtained from $\pi_1$ in Lemma 6.4 of~\cite{EGM:97} by substituting $\textsc{fin}$ for $Order$ and by applying the shift operation in Section 4.5 of~\cite{BD:94}. Let $\Pi^{\diamond}_0$ ($\Pi^{\star}_0$) be the program obtained from $\Pi^{\diamond}$ ($\Pi^{\star}$, respectively) by adding $\textsc{inf}$ ($\textsc{fin}$, respectively) to the body of each rule as a conjunct. Let $\Pi^{\dag}$ be the union of $\Pi^{\diamond}_0$, $\Pi^{\star}_0$, $\Pi_{\mathrm{inf}}$ and $\Pi_{\mathrm{fin}}$. We can show
%$
%\mathrm{SM}(\Pi)\equiv\exists\sigma\mathrm{SM}(\Pi^{\dag})
%$, where $\sigma$ is the set of all constants occurring in $\Pi^{\dag}$ but not in $\Pi$.

Next, let us construct the desired program. Let $\Pi^{\circ}_0$ (respectively $\Pi^{\diamond}_0$) denote the normal program obtained from $\Pi^{\circ}$ (respectively, $\Pi^{\diamond}$) by adding $\textsc{finite}$ (respectively, $\neg\textsc{finite}$) to the body of each rule as a conjunct. Let $\Pi^{\dag}$ be the union of $\Pi^{\circ}_0$, $\Pi^{\diamond}_0$ and $\Pi_{\textsc{t}}$. Let $\nu=\upsilon(\Pi^{\dag})-\upsilon(\Pi)$. Now, we show that $\exists\nu\mathrm{SM}(\Pi^{\dag})$ is equivalent to $\mathrm{SM}(\Pi)$ over arbitrary structures.
By definition and the splitting lemma in \cite{FLLP:09}, it suffices to show that $\mathrm{SM}(\Pi)$ is equivalent to%\vspace{-.1cm}
\begin{equation}
\exists\textsc{finite}[\exists\sigma\mathrm{SM}(\Pi^{\circ}_0)\wedge\exists\tau\mathrm{SM}(\Pi^{\diamond}_0)\wedge\exists\pi\mathrm{SM}(\Pi_{\textsc{t}})].%\vspace{-.1cm}
\end{equation}

Let $\mathds{A}$ be a structure of $\upsilon(\Pi)$. As a strict partial order always exists on domain $A$, we can construct an $\upsilon(\Pi)\cup\upsilon(\Pi_{\textsc{t}})$-expansion $\mathds{B}$ of $\mathds{A}$ such that $\mathds{B}$ is a stable model of $\Pi_{\textsc{t}}$. By the claim, $\mathds{B}\models\textsc{finite}$ if and only if $\mathds{A}$ is finite. First assume that $\mathds{A}$ is finite. By definition, it is clear that $\exists\sigma\mathrm{SM}(\Pi^{\circ}_0)$ is satisfied by $\mathds{B}$ if and only if $\exists\sigma\mathrm{SM}(\Pi^{\circ})$ is satisfied by $\mathds{A}$, and $\exists\sigma\mathrm{SM}(\Pi^{\diamond}_0)$ is always true in $\mathds{B}$. This means that $\exists\nu\mathrm{SM}(\Pi^{\dag})$ is equivalent to $\mathrm{SM}(\Pi)$ over finite structures. By a symmetrical argument, we can show that the equivalence also holds over infinite structures. This then completes the proof.
\end{proof}

\begin{rem}
In classical logic, it is well-known that separating languages over arbitrary structures is usually easier than that over finite structures~\cite{EF:99}. In logic programming, it also seems that arbitrary structures are better-behaved than finite structures. For example, there are some preservation theorems that work on arbitrary structures, but not on finite structures~\cite{AG:94}. Thus, it might be possible to develop techniques on arbitrary structures for some stronger separations of $\mathrm{DLP}$ from $\mathrm{NLP}$.
\end{rem}


%From Theorem \ref{thm:arb_dlp2nlp} and Proposition \ref{prop:fin_dlp2nlp}, we immediately have:

\begin{cor}
$\mathrm{DLP}\simeq\mathrm{NLP}$ iff $\mathrm{NP}=\mathrm{coNP}$.
\end{cor}

%\section{From Second-order Logic to Logic Programs}

Next, we give a characterization for disjunctive programs.

\begin{prop}
$\mathrm{DLP}\simeq\Sigma^{1}_{2}[\forall^{\ast}\exists^{\ast}]$.
\end{prop}

\begin{proof}
(Sketch) The direction ``$\le$" trivially follows from the second-order definition of stable model semantics. So, it remains to show the converse.
Let $\varphi$ be a sentence in $\Sigma${\small$^{1}_{2}$}$[\forall^{\ast}\exists^{\ast}]$. %It suffices to show that there is a disjunctive program $\Pi$ and a finite set $\varsigma$ of auxiliary predicates such that $\exists\varsigma\mathrm{SM}(\Pi)$ is equivalent to $\varphi$.
Without loss of generality, assume that $\varphi$ is of the form%\vspace{-.1cm}
\begin{equation}
\exists\tau\forall\sigma\forall\bar{x}\exists\bar{y}[\vartheta_1(\bar{x},\bar{y})\vee\cdots\vee\vartheta_k(\bar{x},\bar{y})]%\vspace{-.1cm}
\end{equation}
where $\tau$ and $\sigma$ are two finite sets of predicates; $\bar{x}$ and $\bar{y}$ two finite tuples of individual variables; each $\vartheta_i$ is a conjunction of atoms or negated atoms. Let $n$ be the length of $\bar{x}$.

Now, we construct a translation. Firstly, let us define%\vspace{-.1cm}
\begin{equation}
\begin{aligned}
\Lambda_1\,\,&=&\!\!\{&\!\!\!\!\!\!&\,T_X(\bar{x},\bar{z})\vee F_X(\bar{x},\bar{z})\,\, &\mid\,\, X\in\sigma\cup\tau\,&\!\!\!\!\!\!\}&,\\
\Lambda_2\,\,&=&\!\!\{&\!\!\!\!\!\!&D(\bar{x})\rightarrow F_X(\bar{x},\bar{z})\,\, &\mid\,\, X\in\sigma&\!\!\!\!\!\!\}&,\\
\Lambda_3\,\,&=&\!\!\{&\!\!\!\!\!\!&D(\bar{x})\rightarrow T_X(\bar{x},\bar{z})\,\, &\mid\,\, X\in\sigma&\!\!\!\!\!\!\}&,\\
\Lambda_4\,\,&=&\!\!\{&\!\!\!\!\!\!&\vartheta^{\diamond}_i(\bar{x},\bar{y})\rightarrow D(\bar{x})\,\, &\mid\,\, 1\le i\le k&\!\!\!\!\!\!\}&,\\
\Lambda_5\,\,&=&\!\!\{&\!\!\!\!\!\!&\neg D(\bar{x})\rightarrow\bot\,\,&&\!\!\!\!\!\!\}&,
\end{aligned}%\vspace{-.1cm}
\end{equation}
%\begin{center}
%\begin{tabular}{lrcll}
%%  \hline
%  % after \\: \hline or \cline{col1-col2} \cline{col3-col4} ...
%  $\{$ & \!\!$X(\bar{x},\bar{u})\vee X^c(\bar{x},\bar{u})$ & $\mid$ & $X\in\sigma\cup\tau$\!\! & $\}\,\,\cup$ %\vspace{.1cm}\\
%  $\{$ & $D(\bar{x})\rightarrow X(\bar{x},\bar{u})$ & $\mid$ & $X\in\sigma$ & $\}\,\,\cup$ %\vspace{.1cm}\\
%  $\{$ & $D(\bar{x})\rightarrow X^c(\bar{x},\bar{u})$ & $\mid$ & $X\in\sigma$ & $\}\,\,\cup$ %\vspace{.1cm}\\
%  $\{$ & $\vartheta^c_i(\bar{x},\bar{y})\rightarrow D(\bar{x})$ & $\mid$ & $1\le i\le k$ & $\}\,\,\cup$ %\vspace{.1cm}\\
%  $\{$ & $\neg D(\bar{x})\rightarrow\bot$ &  &   & $\}$ \\
%%  \hline
%\end{tabular}
%\end{center}
where, for each $X\in\sigma\cup\tau$, $T_X$ and $F_X$ are two distinct new predicates of arity $(m+n)$ if $m$ is the arity of $X$; each $\vartheta^{\diamond}_i$ is the formula obtained from $\vartheta_i$ by substituting $F_X(\bar{x},\bar{t})$ for $\neg X(\bar{t})$ and followed by substituting $T_X(\bar{x},\bar{t})$ for $X(\bar{t})$ whenever $X\in\sigma\cup\tau$ and $\bar{t}$ is a tuple of terms of the corresponding length; and $D$ is an $n$-ary new predicate.

Let $\Pi$ be the union of $\Lambda_1,\dots,\Lambda_5$. Clearly, $\Pi$ is a disjunctive program. Let $\pi$ be the set of new predicates introduced in the translation. By a similar argument to that in Lemma \ref{lem:so2dlp}, we can show that $\varphi$ is equivalent to $\exists\pi\mathrm{SM}(\Pi)$.
%
%Let $\mathds{A}$ be a model of $\varphi$. Let $\mathds{B}$ be the $\upsilon(\Pi)$-expansion of $\mathds{A}$ in which
%\begin{enumerate}
%\item both predicates $T_X$ and $F_X$ are interpreted to be the full relation of arity $n+m$ if $X$ is an $m$-ary predicate in $\tau\cup\sigma$;
%\item predicate $D$ is interpreted to be the full relation of arity $n$.
%\end{enumerate}
%By a routine check, we can show that $\textsc{Ins}(\mathds{B},\tau)$ is a minimal of $\Pi${\small$^\mathds{B}$}. By Proposition \ref{prop:fo2prop}, $\mathds{B}$ should a stable model of $\Pi$. This implies that $\mathds{A}$ is a model of $\exists\pi\mathrm{SM}(\Pi)$ immediately.
%
%Conversely, let $\mathds{A}$ be a model of $\exists\pi\mathrm{SM}(\Pi)$. By definition, there should exist an $\upsilon(\Pi)$-expansion $\mathds{B}$ of $\mathds{A}$ such that $\mathds{B}$ is a stable model of $\Pi$. Let $\psi$ be the quantifier-free part of $\varphi$, and let $\upsilon_0=\upsilon(\forall\bar{x}\exists\bar{y}\psi)-\tau$. Towards a contradiction, assume that $\mathds{A}$ does not satisfy $\varphi$. Consequently, there must exist an $\upsilon_0$-expansion $\mathds{C}$ and an assignment $\alpha$ in $\mathds{C}$ such that $\alpha$ satisfies $\neg\exists\bar{y}\vartheta_i$ in $\mathds{C}$ for all $i:1\le i\le k$. Let $S$ be the set of ground atoms $F_X(\bar{x},\bar{z})[\alpha_0]$ for all assignments $\alpha_0$ in $\mathds{C}$ that satisfies $X(\bar{z})$ and that coincides with $\alpha$ on $\bar{x}$. Let \begin{equation}
%M=\textsc{Ins}(\mathds{B},\pi)-(S\cup\{D(\bar{x})[\alpha]\}).
%\end{equation}
%It is not difficult to verify that $M$ is a model of $\Pi${\small$^{\mathds{B}}$}. However, according to Proposition \ref{prop:fo2prop}, $\textsc{Ins}(\mathds{B},\pi)$ should be a minimal model of $\Pi${\small$^{\mathds{B}}$}, a contradiction. This completes the proof.
\end{proof}%%\vspace{-.4cm}

%\begin{lem}\label{lem:elem_equv_prv}
%Let $\varphi$ be a sentence in $\Sigma^1_1[\forall^{\ast}]$. Let $\mathds{A}$ and $\mathds{B}$ be two structure of $\upsilon(\varphi)$ such that $\mathds{A}$ is elementary equivalent to $\mathds{B}$. Then $\mathds{A}$ is a model of $\varphi$ iff so is $\mathds{B}$.
%\end{lem}
%
%\begin{proof}
%Due to the duality, it suffices to show one direction. Assume that $\mathds{A}$ is a model of $\varphi$ and $\varphi$ is of form $\exists\tau\forall\bar{x}\vartheta$, where $\vartheta$ is quantifier-free and $\tau$ a finite set of predicates. Then there is a $\sigma$-expansion $\mathds{A}_0$ of $\mathds{A}$ such that $\mathds{A}_0\models\forall\bar{x}\vartheta$.  Let $C=\{\hat{a}\mid a\in B\}$ and $\sigma=\upsilon(\forall\bar{x}\vartheta)\cup C$, where each $\hat{a}$ is a new individual constant. Let $\mathds{B}^{\ast}$ be the $\sigma$-expansion of $\mathds{B}$ that interpreted each $\hat{a}$ as $a$. Let $\Sigma$ be the set of first-order sentences $\gamma$ of $\sigma$ such that $\mathds{B}^{\ast}\models\gamma$. Now we claim:
%
%\medskip
%\noindent{\em Claim}. $\Sigma\cup\{\forall\bar{x}\vartheta\}$ is satisfiable.
%
%\medskip
%Towards a contradiction, assume it is not true. Then by the compactness, there must exist a finite subset $\Phi$ of $\Sigma$ such that $\Phi\cup\{\forall\bar{x}\vartheta\}$ is unsatisfiable. Let $\zeta$ be the conjunction of sentences in $\Phi$. Clearly, the formula $\forall\bar{x}\vartheta\rightarrow\neg\zeta$ is valid.  Let $\bar{c}$ be the tuple of individual constants that appear in both $\zeta$ and $C$. Let $\mathds{A}^{\ast}_0$ be any $\sigma\cup\tau$-expansion of $\mathds{A}_0$, and let $\mathds{A}^{\ast}$ be the restriction of $\mathds{A}^{\ast}_0$ to $\sigma$. As $\mathds{A}_0$ is a model of $\forall\bar{x}\vartheta$, $\mathds{A}^{\ast}_0$ should satisfy $\neg\zeta$, which implies that $\mathds{A}^{\ast}$ is a model of $\neg\zeta$. Since $\mathds{B}$ is elementary equivalent to $\mathds{A}$, this means that $\mathds{B}$ is also a model of $\neg\zeta$, which is impossible since, by the definition of $\Sigma$, $\zeta$ should be in $\Sigma$. Thus, the claim is true.
%
%Let $\mathds{C}$ be a model of $\Sigma\cup\{\forall\bar{x}\vartheta\}$.
%\end{proof}
%
%\begin{prop}
%Let $\Pi$ be a disjunctive program, and let $\mathds{A}$ and $\mathds{B}$ be structures of $\upsilon(\Pi)$ such that $\mathds{A}$ is elementary equivalent to $\mathds{B}$. Then $\mathds{A}$ is a stable model of $\Pi$ iff so is $\mathds{B}$.
%\end{prop}
%
%\begin{proof}
%According to the definition, $\mathrm{SM}(\Pi)$ is equivalent to a formula of the form $\varphi\wedge\neg\psi$, where $\varphi$ is a universal first-order sentence, and $\psi$ a sentence in $\Sigma^1_1[\forall^{\ast}]$. By Lemma \ref{lem:elem_equv_prv}, both $\varphi$ and $\psi$ are closed under elementary equivalence. So, $\mathrm{SM}(\Pi)$ is also closed under elementary equivalence.
%\end{proof}
%
%\begin{thm}
%Let $\Pi$ be a disjunctive program. If $\Pi$ has a stable model, then $\Pi$ has a countable stable model.
%\end{thm}



\section{Conclusion and Related Work}

Combining the results proved in previous sections with some existing results, we then obtain an almost complete picture for the expressiveness of logic programs and some related fragments of second-order logic. As shown in Figure \ref{figure:conclusion}, the expressiveness hierarchy in each subfigure is related to a structure class. In each subfigure, the syntactical classes in a same block are proved to be of the same expressiveness over the related structure class. A block is closer to the top, the classes in the block are then more expressive. In addition, a dashed line means that the corresponding separation is true if and only if $\mathrm{NP}$ is not closed under complement.
%
%
%Except for the intranslatability from disjunctive programs to normal programs with bounded auxiliary constant, the work of this paper can be concluded by Figure \ref{figure:conclusion}.

%\begin{figure}[!h]
%\setlength{\unitlength}{0.115in}
%\begin{minipage}[t]{0.33\linewidth}
%\begin{center}
%\begin{picture}(8.5,13)\thicklines
%\put(0,0){\line(0,1){12.8}}
%\put(8.5,0){\line(0,1){12.8}}
%\put(0,0){\line(1,0){8.5}}
%\put(2,0.6){{\footnotesize$\mathrm{FO}$}}
%\put(0,2){\line(1,0){8.5}}
%\put(2,2.6){{\footnotesize$\Sigma^1_{1\textsc{f}}[\forall^{\ast}]$}}
%\put(2,4.0){{\footnotesize$\Sigma^1_{1}$}}
%\put(0,5.5){\line(1,0){8.5}}
%\put(2,6.3){{\footnotesize$\mathrm{NLP}$}}
%\put(2,7.7){{\footnotesize$\mathrm{DLP}$}}
%\put(2,9.1){{\footnotesize$\Sigma^1_2[\forall^{\ast}\exists^{\ast}]$}}
%\put(0,10.7){\line(1,0){8.5}}
%\put(2,11.3){{\footnotesize$\Sigma^1_2$}}
%\put(0,12.8){\line(1,0){8.5}}
%\end{picture}\\
%{\footnotesize Infinite Structures}
%\end{center}
%\end{minipage}%
%\begin{minipage}[t]{0.33\linewidth}
%\begin{center}
%\begin{picture}(8.5,13)\thicklines
%\put(0,0){\line(0,1){12.8}}
%\put(8.5,0){\line(0,1){12.8}}
%\put(0,0){\line(1,0){8.5}}
%\put(2,0.6){{\footnotesize$\mathrm{FO}$}}
%\put(0,2){\line(1,0){8.5}}
%\put(2,2.8){{\footnotesize$\Sigma^1_{1\textsc{f}}[\forall^{\ast}]$}}
%\put(2,4.2){{\footnotesize$\Sigma^1_{1}=\mathrm{NP}$}}
%\put(2,5.6){{\footnotesize$\mathrm{NLP}$}}
%\put(0,7.3){\dashbox{0.2}(8.5,0){}}
%\put(2,8.2){{\footnotesize$\mathrm{DLP}$}}
%\put(2,9.6){{\footnotesize$\Sigma^1_2[\forall^{\ast}\exists^{\ast}]$}}
%\put(2,11.0){{\footnotesize$\Sigma^1_2=\Sigma^p_2$}}
%\put(0,12.8){\line(1,0){8.5}}
%\end{picture}\\
%{\footnotesize Finite Structures}
%\end{center}
%\end{minipage}%
%\begin{minipage}[t]{0.33\linewidth}
%\begin{center}
%\begin{picture}(8.5,13)\thicklines
%\put(0,0){\line(0,1){12.8}}
%\put(8.5,0){\line(0,1){12.8}}
%\put(0,0){\line(1,0){8.5}}
%\put(2,0.6){{\footnotesize$\mathrm{FO}$}}
%\put(0,2){\line(1,0){8.5}}
%\put(2,2.6){{\footnotesize$\Sigma^1_{1\textsc{f}}[\forall^{\ast}]$}}
%\put(2,4.0){{\footnotesize$\Sigma^1_{1}$}}
%\put(0,5.5){\line(1,0){8.5}}
%\put(2,6.0){{\footnotesize$\mathrm{NLP}$}}
%\put(0,7.3){\dashbox{0.2}(8.5,0){}}
%\put(2,7.8){{\footnotesize$\mathrm{DLP}$}}
%\put(2,9.2){{\footnotesize$\Sigma^1_2[\forall^{\ast}\exists^{\ast}]$}}
%\put(0,10.7){\line(1,0){8.5}}
%\put(2,11.3){{\footnotesize$\Sigma^1_2$}}
%\put(0,12.8){\line(1,0){8.5}}
%\end{picture}\\
%{\footnotesize Arbitrary Structures}
%\end{center}
%\end{minipage}%
%\caption{Expressiveness Hierarchies Related to LPs}
%\end{figure}

\begin{figure}[!h]%\vspace{-.2cm}
\setlength{\unitlength}{0.115in}
\begin{minipage}[t]{0.33\linewidth}
\begin{center}
\begin{picture}(8.5,11)\thicklines
\put(0,0){\line(0,1){10.8}}
\put(8.5,0){\line(0,1){10.8}}
\put(0,0){\line(1,0){8.5}}
\put(2,0.6){{\footnotesize$\Sigma^{1\textsc{f}}_{1}[\forall^{\ast}]$}}
\put(2,2.0){{\footnotesize$\Sigma^1_{1}$}}
\put(0,3.5){\line(1,0){8.5}}
%\put(0,5.3){\dashbox{0.08}(8.5,0){}}
\put(2,4.1){{\footnotesize$\mathrm{NLP}$}}
\put(2,5.6){{\footnotesize$\mathrm{DLP}$}}
\put(2,7.1){{\footnotesize$\Sigma^1_2[\forall^{\ast}\exists^{\ast}]$}}
\put(0,8.6){\line(1,0){8.5}}
\put(2,9.3){{\footnotesize$\Sigma^1_2$}}
\put(0,10.8){\line(1,0){8.5}}
\end{picture}\\
{\footnotesize Infinite Structures}
\end{center}
\end{minipage}%
\begin{minipage}[t]{0.33\linewidth}
\begin{center}
\begin{picture}(8.5,11)\thicklines
\put(0,0){\line(0,1){10.8}}
\put(8.5,0){\line(0,1){10.8}}
\put(0,0){\line(1,0){8.5}}
\put(2,0.8){{\footnotesize$\Sigma^{1\textsc{f}}_{1}[\forall^{\ast}]$}}
\put(2,2.3){{\footnotesize$\Sigma^1_{1}=\mathrm{NP}$}}
\put(2,3.8){{\footnotesize$\mathrm{NLP}$}}
\put(0,5.3){\dashbox{0.2}(8.5,0){}}
\put(2,6.1){{\footnotesize$\mathrm{DLP}$}}
\put(2,7.6){{\footnotesize$\Sigma^1_2[\forall^{\ast}\exists^{\ast}]$}}
\put(2,9.1){{\footnotesize$\Sigma^1_2=\Sigma^p_2$}}
\put(0,10.8){\line(1,0){8.5}}
\end{picture}\\
{\footnotesize Finite Structures}
\end{center}
\end{minipage}%
\begin{minipage}[t]{0.33\linewidth}
\begin{center}
\begin{picture}(8.5,11)\thicklines
\put(0,0){\line(0,1){10.8}}
\put(8.5,0){\line(0,1){10.8}}
\put(0,0){\line(1,0){8.5}}
\put(2,0.6){{\footnotesize$\Sigma^{1\textsc{f}}_{1}[\forall^{\ast}]$}}
\put(2,2.0){{\footnotesize$\Sigma^1_{1}$}}
\put(0,3.5){\line(1,0){8.5}}
\put(2,4.0){{\footnotesize$\mathrm{NLP}$}}
\put(0,5.3){\dashbox{0.2}(8.5,0){}}
\put(2,5.8){{\footnotesize$\mathrm{DLP}$}}
\put(2,7.2){{\footnotesize$\Sigma^1_2[\forall^{\ast}\exists^{\ast}]$}}
\put(0,8.6){\line(1,0){8.5}}
\put(2,9.3){{\footnotesize$\Sigma^1_2$}}
\put(0,10.8){\line(1,0){8.5}}
\end{picture}\\
{\footnotesize Arbitrary Structures}
\end{center}
\end{minipage}%\vspace{-.2cm}
\caption{Expressiveness Hierarchies Related to LPs}\label{figure:conclusion}%\vspace{-.2cm}
\end{figure}

Without involving the well-known complexity conjecture, we established the intranslatability from disjunctive to normal programs over finite structures if the arities of auxiliary constants are bounded in a certain sense. This can be regarded as evidence that disjunctive programs are more expressive than normal programs over finite structures. As a byproduct, we also developed a succinct translation from normal programs to first-order sentences. This then improved the ordered completion proposed by~\cite{ALZZ:12}.


There are several existing works contributing to Figure \ref{figure:conclusion}, which are listed as follows. The translatability from $\Sigma${\small$^1_1$} to $\Sigma${\small$^{1\textsc{f}}_1$}$[\forall^{\ast}\hspace{-.03cm}]$ follows from the well-known Skolem normal form. The translatability from $\Sigma^1_2$ to $\Sigma${\small$^1_2$}$[\forall^{\ast}\hspace{-.03cm}\exists^{\ast}\hspace{-.03cm}]$ over finite structures is due to~\cite{Leiv:89}. The separation of $\Sigma${\small$^1_2$} from $\Sigma${\small$^1_2$}$[\forall^{\ast}\hspace{-.03cm}\exists^{\ast}\hspace{-.03cm}]$ (on both arbitrary and infinite structures) is due to~\cite{EGG:96}. From $\mathrm{NLP}$ to $\Sigma${\small$^1_1$}, both the intranslatability over arbitrary structures and the translatability over finite structures are due to~\cite{ALZZ:12}.

%{\footnotesize$\Sigma^1_2[\forall^{\ast}\exists^{\ast}]$\\$\mathrm{DLP}$}}

%%Results in this paper ...
%To the best of our knowledge, the weaker separation over finite structures in this paper gives us the first lower bound for arities of auxiliary predicates in the translatability from disjunctive logic programs into normal logic programs. Improving the lower bound will shed light on deeply understanding the expressive power of disjunctive and normal logic programs, which will be a challenging task in the further study. The equivalence of the translatability over finite structures and over arbitrary structures provides us a new perspective to achieve this goal. We will pursue this in the future.

The (in)translatability between first-order theories and logic programs were also considered in~\cite{ZZYZ:11}. But first-order theories there are based on non-monotonic semantics. Over Herbrand structures, \cite{Schl:95,EG:97} proved that normal programs, disjunctive programs and universal second-order logic are of the same expressiveness under the query equivalence. Their proofs employ an approach from  recursion theory. However, this approach seems difficult to be applied to general infinite structures. In the propositional case, there have been a lot of works on the translatability and expressiveness of logic programs, e.g., \cite{EFTW:04,Janhunen:06}. It should be noted that the picture of expressiveness and translatability in there is quite different from that in the first-order case.


%This is because, as shown in Figure \ref{figure:conclusion}, over infinite structures, normal programs are separated from Our result over infinite structures is more general and stronger than theirs as Herbrand structures are only a special class of countable infinite structures. It is not clear whether or not their approach, which employs the inductive definability from~\cite{Barw:76,Mosc:74}, can be generalized to arbitrary infinite structures.

{%\small
\bibliographystyle{amsplain}
\bibliography{kr}
}

\end{document}

lp_exp.bbl
\providecommand{\bysame}{\leavevmode\hbox to3em{\hrulefill}\thinspace}
\providecommand{\MR}{\relax\ifhmode\unskip\space\fi MR }
% \MRhref is called by the amsart/book/proc definition of \MR.
\providecommand{\MRhref}[2]{%
  \href{http://www.ams.org/mathscinet-getitem?mr=#1}{#2}
}
\providecommand{\href}[2]{#2}
\begin{thebibliography}{10}

\bibitem{Ajtai:83}
M.~Ajtai, \emph{{$\Sigma^1_1$}-formulae on finite structures}, Annals of Pure
  and Applied Logic \textbf{24} (1983), 1--48.

\bibitem{AG:94}
M.~Ajtai and Y.~Gurevich, \emph{Datalog vs first-order logic}, Journal of
  Computer and System Sciences \textbf{49} (1994), 562--588.

\bibitem{ALZZ:12}
V.~Asuncion, F.~Lin, Y.~Zhang, and Y.~Zhou, \emph{Ordered completion for
  first-order logic programs on finite structures}, Artificial Intelligence
  \textbf{177--179} (2012), 1--24.

\bibitem{BD:94}
R.~Ben-Eliyahu and R.~Dechter, \emph{Propositional semantics for disjunctive
  logic programs}, Annals of Mathematics and Artificial Intelligence
  \textbf{12} (1994), no.~1--2, 53--87.

\bibitem{DEGV:01}
E.~Dantsin, T.~Eiter, G.~Gottlob, and A.~Voronkov, \emph{Complexity and
  expressive power of logic programming}, ACM Computing Surveys \textbf{33}
  (2001), no.~3, 374--425.

\bibitem{DGO:04}
A.~Durand, E.~Grandjean, and F.~Olive, \emph{New results on arity vs. number of
  variables}, Research report 20--2004, LIF, \textbf{Marseille, France} (2004).

\bibitem{DLS:98}
A.~Durand, C.~Lautemann, and T.~Schwentick, \emph{Subclasses of binary {NP}},
  Journal of Logic and Computation \textbf{8} (1998), no.~2, 189--207.

\bibitem{EF:99}
H.-D. Ebbinghaus and J.~Flum, \emph{Finite model theory}, 2 ed.,
  Springer-Verlag, New York, 1999.

\bibitem{EG:97}
T.~Eiter and G.~Gottlob, \emph{Expressiveness of stable model semantics for
  disjunctive logic programs with functions}, The Journal of Logic Programming
  \textbf{33} (1997), 167--178.

\bibitem{EGG:96}
T.~Eiter, G.~Gottlob, and Y.~Gurevich, \emph{Normal forms for second-order
  logic over finite structures, and classication of {NP} optimization
  problems}, Annals of Pure and Applied Logic \textbf{78} (1996), 111--125.

\bibitem{EGM:97}
T.~Eiter, G.~Gottlob, and H.~Mannila, \emph{Disjunctive datalog}, ACM
  Transactions on Database Systems \textbf{22} (1997), 364--418.

\bibitem{EFTW:04}
Thomas Eiter, Michael Fink, Hans Tompits, and Stefan Woltran, \emph{On
  eliminating disjunctions in stable logic programming}, Proceedings of KR,
  2004, pp.~447--458.

\bibitem{Fagin:74}
R.~Fagin, \emph{Generalized first-order spectra and polynomial-time
  recognizable sets}, Complexity of Computation, SIAM-AMS Proceedings, vol.~7,
  1974, pp.~43--73.

\bibitem{FLL:11}
P.~Ferraris, J.~Lee, and V.~Lifschitz, \emph{Stable models and
  circumscription}, Artificial Intelligence \textbf{175} (2011), 236--263.

\bibitem{FLLP:09}
P.~Ferraris, J.~Lee, V.~Lifschitz, and R.~Palla, \emph{Symmetric splitting in
  the general theory of stable models}, Proceedings of IJCAI, 2009,
  pp.~797--803.

\bibitem{GL:88}
M.~Gelfond and V.~Lifschitz, \emph{The stable model semantics for logic
  programming}, Proceedings of ICLP/SLP, 1988, pp.~1070--1080.

\bibitem{Gran85}
Etienne Grandjean, \emph{Universal quantifiers and time complexity of random
  access machines}, Mathematical Systems Theory \textbf{18} (1985), no.~2,
  171--187.

\bibitem{Imme:99}
Neil Immerman, \emph{Descriptive complexity}, Graduate texts in computer
  science, Springer, 1999.

\bibitem{Janhunen:06}
Tomi Janhunen, \emph{Some (in)translatability results for normal logic programs
  and propositional theories}, Journal of Applied Non-Classical Logics
  \textbf{16} (2006), no.~1--2, 35--86.

\bibitem{Leiv:89}
D.~Leivant, \emph{Descriptive characterizations of computational complexity},
  Journal of Computer and System Sciences \textbf{39} (1989), 51--83.

\bibitem{LM:04}
Yuliya Lierler and Marco Maratea, \emph{Cmodels-2: {SAT}-based answer set
  solver enhanced to non-tight programs}, Proceedings of LPNMR, 2004,
  pp.~346--350.

\bibitem{LZ:04}
F.~Lin and Y.~Zhao, \emph{Assat: computing answer sets of a logic program by
  sat solvers}, Artificial Intelligence \textbf{157} (2004), no.~1-2, 115--137.

\bibitem{LZ:11}
F.~Lin and Y.~Zhou, \emph{From answer set logic programming to circumscription
  via logic of {GK}}, Artificial Intelligence \textbf{175} (2011), no.~1,
  264--277.

\bibitem{LMR:92}
J.~Lobo, J.~Minker, and A.~Rajasekar, \emph{Foundations of disjunctive logic
  programming}, The MIT Press, Cambridge, 1992.

\bibitem{PV:05}
David Pearce and Agust��n Valverde, \emph{A first order nonmonotonic extension
  of constructive logic}, Studia Logica \textbf{80} (2005), no.~2/3, 321--346.

\bibitem{Schl:95}
J.~S. Schlipf, \emph{The expressive powers of the logic programming semantics},
  Journal of Computer and System Sciences \textbf{51} (1995), no.~1, 64--86.

\bibitem{Stoc:77}
L.~J. Stockmeyer, \emph{The polynomial-time hierarchy}, Theoretical Computer
  Science \textbf{3} (1977), 1--22.

\bibitem{ZZ:13}
Heng Zhang and Yan Zhang, \emph{First-order expressibility and boundedness of
  disjunctive logic programs}, Proceedings of IJCAI, 2013, pp.~1198--1204.

\bibitem{ZZYZ:11}
Heng Zhang, Yan Zhang, Mingsheng Ying, and Yi~Zhou, \emph{Translating
  first-order theories into logic programs}, IJCAI, 2011, pp.~1126--1131.

\end{thebibliography}
