# Comparing the Reasoning Capabilities of Equilibrium Theories and Answer Set Programs
## 3 Equivalence Notions  
Based on these relations, we now can define different notions of equivalence between theories. Definition 4: Let \(\Pi_{1}\) and \(\Pi_{2}\) be theories and \(\alpha\in\{c,s,p\}\). Then, \(\Pi_{1}\equiv_{a}\Pi_{2}\) states that for any formula \(\varphi\), \(\Pi_{1}\models_{a}\varphi\) iff \(\Pi_{2}\models_{a}\varphi\). \({}_{\blacksquare}\)  
We are now able to compare theories in further different ways:  
Definition 5: Let \(\Pi_{1}\) and \(\Pi_{2}\) be theories and \(\alpha\in\{c,s,p\}\). Then,  
* \(\Pi_{1}\equiv^{s}\Pi_{2}\) holds iff for any further theory \(\Pi\), \((\Pi_{1}\cup\Pi)\equiv(\Pi_{2}\cup\Pi)\). * \(\Pi_{1}\equiv^{u}\Pi_{2}\) holds iff for any set \(X\) of atoms, \((\Pi_{1}\cup X)\equiv(\Pi_{2}\cup X)\). * \(\Pi_{1}\equiv^same **HT** models [2]. Uniform equivalence on the other hand is captured by a special set of **HT** countermodels [26] (see also [3; 27]). Evidently, if theories are equivalent, then their inference relations are also equivalent for all types of inference. However, what happens if two theories have different equilibrium models; can we always separate them in terms of sentences they entail? The following lemma answers this in the affirmative for credulous and sceptical inference. To simplify notation, we treat an equilibrium model as a set of atoms \(M\). **Lemma 1**. : _Let \(\Pi_{1}\) and \(\Pi_{2}\) be stable theories such that \(E(\Pi_{1})\
eq E(\Pi_{2})\); say that \(\Pi_{1}\) has an equilibrium model \(M\) that is not an equilibrium model of \(\Pi_{2}\). Then:_  
_(i) There exists a sentence \(\varphi\) such that \(M\models\varphi\) but \(\varphi\) is false in all equilibrium models of \(\Pi_{2}\). Hence, \(\Pi_{1}\models_{c}\varphi\), \(\Pi_{2}\
ot\models_{c}\varphi\), and so \(\Pi_{1}\
ot\equiv_{c}\Pi_{2}\)._  
_(ii) There exists a sentence \(\psi\) such that \(M\
ot\models\psi\) but \(M_{i}\models\psi\) for each equilibrium model \(M_{i}\in E(\Pi_{2})\). Hence, \(\Pi_{2}\models_{s}\psi\) whereas \(\Pi_{1}\
ot\models_{s}\psi\) and so \(\Pi_{1}\
ot\equiv_{s}\Pi_{2}\)._  
Proof. : (i) For each \(M_{i}\in E(\Pi_{2})\), we know that \(M\cap(U\setminus M_{i})\
eq\emptyset\) or \(M_{i}\cap(U\setminus M)\
eq\emptyset\) with \(U=At(\Pi_{1}\cup\Pi_{2})\). Set  
\[\varphi_{i}=\bigwedge_{a\in M\cap(U\setminus M_{i})}a\wedge\bigwedge_{b\in M_{ i}\cap(U\setminus M)}\
eg b\]  
Then, \(M\models\varphi_{i}\), for each \(i\), so \(M\models\varphi\) where \(\varphi=\bigwedge\varphi_{i}\) and \(\Pi_{1}\models_{c}\varphi\). However, for any \(M_{i}\in E(\Pi_{2})\), \(M_{i}\
ot\models\varphi\) which implies that \(\Pi_{2}\
ot\models_{c}\varphi\). (ii) Similarly, for each equilibrium model \(M_{i}\) of \(\Pi_{2}\) either there is some atom \(a\in M\) such that \(M_{i}\models\
eg a\) or else there is some atom \(b\in U\setminus M\) such that \(M^{\prime}\models b\), where \(U\) is the set of atoms in \(\Pi_{1}\cup\Pi_{2}\). Set  
\[\psi_{i}=\bigvee_{a\in M\cap(U\setminus M_{i})}\
eg a\vee\bigvee_{b\in(U \setminus M)\cap M_{i}}b\]  
Then, \(\psi=\bigvee\psi_{i}\) holds in each equilibrium model of \(\Pi_{2}\) and so \(\Pi_{2}\models_{s}\psi\). By inspection \(M\
ot\models\psi\) and so \(\Pi_{1}\
ot\models_{s}\psi\). Now it is straightforward to characterise entailment equivalence. **Proposition 2**. : _The following conditions hold:_  
* \(\Pi_{1}\equiv_{c}\Pi_{2}\) _iff_ \(\Pi_{1}\equiv_{s}\Pi_{2}\) _iff_ \(E(\Pi_{1})=E(\Pi_{2})\)_._
* \(\Pi_{1}\equiv_{\alpha}\Pi_{2}\) _implies_ \(\Pi_{1}\equiv_{p}\Pi_{2}\) _for_ \(\alpha\in\{c,s\}\)_._  
The next results show that in the strong-equivalence setting, the choice of the consequence operator does not play a role. Together with the observation from above, we conclude that all three notions are characterised by the logic of here-and-there. **Proposition 3**. : _The following propositions are equivalent:_  
_(i)_ \(\Pi_{1}\equiv^{s}\Pi_{2}\)_;_  
_(ii)_ \(\Pi_{1}\equiv^{s}_{c}\Pi_{2}\)_;_  
_(iii)_ \(\Pi_{1}\equiv^{s}_{s}\Pi_{2}\)_;_  
_(iv)_ \(\Pi_{1}\equiv^{s}_{p}\Pi_{2}\)_._Proof.