\documentstyle[jair,twoside,11pt,theapa]{article}

\jairheading{8}{1998}{1-21}{8/97}{1/98}
\ShortHeadings{Monotonicity and Persistence in Preferential Logics }
{Engelfriet}
\firstpageno{1}


%-----d-e-c-l-a-r-a-t-i-o-n-s-----------------------------------

\newtheorem{theorem}{Theorem}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{example}{Example}
\newtheorem{assumption}{Assumption}

\newcommand{\nminfrel}{\mathbin{{\mid\mkern-9mu\lower0.1ex\hbox{$\sim$}}}}
\newcommand{\Lang}{{\cal L}}
\newcommand{\Mod}{\mbox{\it Mod}}
\newcommand{\satisf}{\models}
\newcommand{\prefto}{\preceq}
\newcommand{\prefent}{\models_{\prefto}}
\newcommand{\Implies}{\Rightarrow}
\newcommand{\Iff}{\Leftrightarrow}
\newcommand{\LangSfive}{\Lang_{\mbox{\tiny S5}}}
\newcommand{\Sfsat}{\models_{\mbox{\tiny S5}}}
\newcommand{\IS}{\mbox{\it IS}}
\newcommand{\peGrSf}
		{\models^{\mbox{\tiny GS5}}}
\newcommand{\LangTEL}{\Lang_{\mbox{\tiny TEL}}}
\newcommand{\nn}{\mbox{{\bf N}}}
\newcommand{\TCIS}{\mbox{\it TCIS}}
\newcommand{\peMTEL}
		{\models^{\mbox{\tiny MTEL}}}
\newcommand{\preftopred}[1]{\leq_{#1}}
\newcommand{\pePCirc}[1]
	{\models_{#1}^{\mbox{\tiny PC}}}
\newcommand{\preftodom}{\leq_{d}}
\newcommand{\peDCirc}
	{\models^{\mbox{\tiny DC}}}
\newcommand{\DIAM}{\mbox{\it DIAM}}
\newcommand{\BOX}{\mbox{\it BOX}}
\newcommand{\TD}{\mbox{\it TD}}
\newcommand{\TB}{\mbox{\it TB}}
\newcommand{\bproof}{\noindent {\bf Proof:\ \ }}
\newcommand{\eproof}{\hfill $\Box$ \vspace{0.5cm}}
\newcommand{\telM}{{\cal M}}
\newcommand{\telN}{{\cal N}}
\newcommand{\telMti}{{\cal M}^{ti}}
\newcommand{\Succ}{\mbox{\it Succ}}
\newcommand{\integers}{\mbox{{\bf Z}}}


\renewcommand{\phi}{\varphi}



\begin{document}

\title{Monotonicity and Persistence in Preferential Logics}

\author{\name Joeri Engelfriet
	\email joeri@cs.vu.nl \\
	\addr Vrije Universiteit, Faculty of Mathematics and 
	      Computer Science \\
	      De Boelelaan 1081a, 1081 HV Amsterdam,
	      The Netherlands}

\maketitle


\begin{abstract}
\noindent
An important characteristic of many logics for Artificial Intelligence 
is their nonmonotonicity. This means that adding a formula to 
the premises can invalidate some of the consequences. There may, 
however, exist formulae that can always be safely added to the 
premises without destroying any of the consequences: we say they respect 
monotonicity. Also, there may be formulae that, when they are a 
consequence, can not be invalidated when adding any formula to the 
premises: we call them conservative. We study these two classes 
of formulae for
preferential logics, and show that they are closely linked to the 
formulae whose truth-value is preserved along the (preferential) 
ordering. We will consider some preferential logics for illustration, 
and prove syntactic characterization results for them. The results in 
this paper may improve the efficiency of theorem provers for 
preferential logics.
\end{abstract}


\section{Introduction}

Over the past decades, many non-classical logics for Artificial 
Intelligence have been defined and investigated. The need for such 
logics arose from the unsuitability of classical logics to describe 
defeasible reasoning.  These classical logics are monotonic, which 
means that their consequence relation ($\nminfrel$) satisfies:\\

\hspace{2.5cm}
$\forall \alpha, \beta, \phi:    ( \alpha \nminfrel \beta \Implies \alpha \land 
\phi  \nminfrel \beta  )$  
\hspace*{\fill}
({\em Monotonicity}) \\

\noindent
This means that whenever we learn new information ($\phi$) and add 
this to what we already know ($\alpha$), all the old theorems 
($\beta$)  are still derivable. This is clearly undesirable when 
describing defeasible reasoning. Therefore, monotonicity is not 
satisfied by many logics for Artificial Intelligence.

On the other hand, monotonicity is a very attractive feature from 
a practical point of view. When learning new information, we do not 
have to start all over again, but we can retain our old conclusions, 
and focus on deriving possible new ones. Furthermore, when we have a lot 
of information, we are allowed to focus on only part of it.
Conclusions derived from this part are then automatically also valid 
when considering all the information we have (this is sometimes 
called {\em local reasoning}).

Even though it is clear that we do not want monotonicity to hold 
in general, it might be worthwhile to investigate restricted variants of 
monotonicity. In the past, such variants have been defined which 
allow us to keep the old theorems, when either the new information 
follows from the old premise \cite<this variant is called Cautious 
Monotonicity by>{KLM90}
or its negation can not be derived 
from the old premise \cite<this is called Rational Monotonicity by>{KLM90}. 

We will take a somewhat different perspective, and 
consider two classes of formulae: the class of formulae that  can 
always be added to a premise without invalidating old conclusions 
(we say these formulae {\em respect monotonicity}), and the class of 
formulae which can always be retained as conclusions, no matter 
which new information is added to the premise (we say these 
formulae are {\em conservative}). The advantages of monotonicity 
sketched above would still hold when we restrict  $\phi$  to the class of 
formulae that respect monotonicity, or when we restrict  $\beta$  to be 
conservative. Whether such classes exist, and what these classes are, 
depends of course on the particular nonmonotonic logic considered.
We will focus here on an important class of nonmonotonic 
logics: the class of {\em preferential logics} \cite{Sh87,Sh88}. 
These logics are based on a monotonic logic (such as 
propositional logic, predicate logic or modal logic) augmented with a 
preference order on its models. The nonmonotonic consequences of 
a formula  $\alpha$  are those formulae which are true in all models of  
$\alpha$  which are minimal in the preference order 
among all models of  $\alpha$ 
\cite<an extensive discussion of preferential logics is provided by>{Be89}. 
We will give a formal definition. 

\begin{definition}[Preferential logic]\label{def:preflog}
A preferential logic consists of a language  $\Lang$, a class of 
models  $\Mod$ together with a satisfaction relation  $\satisf$  
between models and formulae, and a partial order  $\prefto$  on  
$\Mod$. A model  $m \in \Mod$  is called a {\em minimal 
model} of a formula  $\alpha$  (denoted  $m \prefent \alpha$)  if  
$m \satisf \alpha$  and for all models  $n$, if  $n \prefto m$  and  
$n \satisf \alpha$  then  $n = m$. Preferential entailment  
($\prefent$) between formulae is defined as follows: for  $\alpha, 
\beta  \in  \Lang:  \alpha \prefent \beta$  if  $\beta$  is true in all 
minimal models of  $\alpha$.
\end{definition}

Our presentation uses a partial order, i.e., a
reflexive, antisymmetric and transitive relation. \citeauthor{Sh87}
\citeyear{Sh87} uses a
strict partial order, i.e., an irreflexive transitive relation, with a
slightly different notion of minimal model. The presentations can be
translated into each other.

It will turn out that formulae whose truth is preserved when going to 
more preferred or less preferred models, play an important role with 
respect to the two classes of formulae defined above (the class
of formulae that respect monotonicity, and the class of conservative
formulae). We will first give a definition.

\begin{definition}[Persistence]
Given a preferential logic $(\Lang, \Mod, \satisf, \prefto)$,
a formula  $\alpha \in \Lang$  is called {\em downward persistent} in
this logic, if
\[
\forall m, n \in \Mod:  (m \satisf \alpha \mbox{ and }  n \prefto m)  
\Implies  n \satisf \alpha,
\]
and it is called {\em upward persistent} if
\[
\forall m, n \in \Mod:  (n \satisf \alpha  \mbox{ and }  n \prefto m)  
\Implies  m \satisf \alpha.
\]
\end{definition}


In the next section, we will introduce some preferential logics to 
illustrate the material in the rest of the paper. In 
Section~\ref{sec:respmon} we will consider formulae that respect 
monotonicity, and in Section~\ref{sec:cons} conservative formulae 
will be treated. The practical implications of the results of this paper 
are discussed in Section~\ref{sec:pracimpl}. Section~\ref{sec:concl} 
gives conclusions and suggestions for further research. Part of the 
material in this paper appeared in \cite{En96b}.


\section{Some Preferential Logics}\label{sec:preflogs}

In this section we will describe the following preferential logics: 
Ground S5, Minimal Temporal Epistemic Logic and 
Circumscription. Since we have already defined preferential 
entailment in general, for each logic we only have to give its 
ingredients, i.e., $\Lang, \Mod, \satisf$, and $\prefto$.  
The preferential entailment relation is then fixed by 
Definition~\ref{def:preflog}. The first logic we 
will consider is Ground S5.


\subsection{Ground S5}

Ground S5 is a nonmonotonic modal logic for auto-epistemic 
reasoning, originally proposed by Halpern and Moses \citeyear{HM85}. 
Their aim was to formalize statements of the form "I {\em only} 
know  $\phi$". It allows, for example, to derive that an agent which 
only knows  $p$, does not know $q$. Ground S5 falls into the 
general scheme of ground nonmonotonic modal logics 
\cite{DNR95}. A lot of interest is devoted to logics of minimal 
knowledge \cite{Le90,ST94,Ch97,Ha97}. 

Semantically, states in which an agent only knows  $\phi$, are states 
in which  $\phi$  is known, but otherwise the amount of knowledge 
is minimal. We will use a modal propositional language to express 
the knowledge of the agent, and S5  will be the monotonic logic. We 
will give a treatment of Ground S5 slightly different, but equivalent 
to the one given by \citeauthor{HM85} \citeyear{HM85}.

\begin{definition}[Epistemic language]
Let  $P$  be a (finite or countably infinite) set of propositional 
atoms. The language  $\LangSfive$  is the smallest set closed 
under:
\begin{itemize}
\item if  $p \in P$  then  $p \in \LangSfive$;
\item if  $\phi, \psi \in \LangSfive$ then  $K\phi, \phi \land \psi, 
\neg \phi \in \LangSfive$.
\end{itemize}
Furthermore, we introduce the following abbreviations:
\[
\phi \lor \psi \equiv \neg (\neg \phi \land \neg \psi), \phi \to \psi 
\equiv \neg \phi \lor \psi, M\phi \equiv \neg K\neg \phi, \top \equiv 
p \lor \neg p, \bot \equiv \neg \top.
\]
If every atom occurring in a formula  $\phi$  is in the scope of a  
$K$  operator, we call  $\phi$  {\em subjective}.
\end{definition}


An example of a subjective formula is  $\neg Kp \land K(q \to p)$, 
whereas  $K(p \land q) \lor s$  is not subjective. In the rest of this 
paper we will only be interested in subjective formulae: they 
describe (just) the knowledge and ignorance of the agent. 

In the usual S5 semantics, a model is a triple  $(W, R, \pi )$,  where  
$W$  is a set of worlds,  $R$  is an equivalence relation on  $W$  and  
$\pi$  is a function that assigns a propositional valuation to each 
world in  $W$. We may however, in the case of one agent, restrict 
ourselves to {\em normal} S5 models, in which the relation is 
universal (each world is accessible from every world), and worlds 
are identified with propositional valuations 
\cite<a proof of soundness and completeness of S5 with respect 
to these semantics is given by>{MH95}.

\begin{definition}[S5 semantics]
Let $P$ be a (finite or countably infinite) set of propositional
atoms.  A propositional valuation  is a function from  
$P$  into $\{ 0,1 \}$ where $0$ stands for false and $1$ for true. 
The set of all such valuations will be denoted by  $Mod(P)$. A 
normal S5 model  $M$  is a non-empty subset of  $Mod(P)$. The 
truth of an S5 formula  $\phi$  in such a model, evaluated in a 
world  $m \in M$, denoted  $(M, m) \Sfsat \phi$,  is defined 
inductively:
\[
\begin{array}{llll}
1. & (M, m) \Sfsat p  & \Iff & m(p) = 1 \mbox{, for } p \in P \\
2. & (M, m) \Sfsat \phi \land \psi & \Iff & (M, m) \Sfsat \phi  \mbox{ 
and } (M, m) \Sfsat \psi \\
3. & (M, m) \Sfsat \neg \phi & \Iff & \mbox{ it is not the case that } 
(M, m) \Sfsat \phi \\
4. & (M, m) \Sfsat K\phi & \Iff & (M, m') \Sfsat \phi \mbox{ for 
every }  m' \in M
\end{array}
\]
\end{definition}


We have the following elementary results on subjective formulae. 
The proofs are straightforward.

\begin{proposition}[Subjective formulae]\label{def:subjform}~
\begin{enumerate}
\item  Let  $\phi$  be a subjective formula. For a normal S5 model  
$M$  and  $m_{1}, m_2 \in M$   it holds:
\[
(M, m_1) \Sfsat \phi    \Iff    (M, m_2) \Sfsat \phi.
\]
We define  $M \Sfsat \phi$  if  $(M, m) \Sfsat \phi$  for some, or, 
equivalently, all  $m \in M$. The set of all normal S5 models,
sometimes called {\em information states}, is 
denoted by  $\IS$.
\item  An S5 formula  $\phi$  is subjective if and only if it is 
equivalent to a formula of the form  $K\phi$  with  $\phi \in 
\LangSfive$.
\end{enumerate}
\end{proposition}

A subjective formula describes the knowledge of an agent, but we 
want to formalize that this is {\em all} the agent knows. Therefore 
we are looking for models in which the knowledge of the agent is
minimal, or in other words, in which the ignorance of the agent is 
maximal. We introduce a preference order over information states 
which favors models with less knowledge. The definition of this 
ordering is based on the observation that the more valuations the 
agent considers possible, the less knowledge the agent has. Indeed, 
for any propositional formula  $\phi$  we have: if  $M_1 \models K\phi$  
and  $M_1 \supseteq M_2$   then  $M_2 \models K\phi$.

\begin{definition}[Degree of knowledge]\label{def:degofkn} 
We define the {\em degree-of-knowledge} ordering  $\prefto$  
on normal S5 models as follows:  for  $M_1, M_2 \in \IS :     M_1 
\prefto M_2   \Iff   M_1 \supseteq M_2$.
\end{definition}


Ground S5 is the preferential logic based on this ordering.

\begin{definition}[Ground S5]
Ground S5 is the preferential logic with the subjective formulae 
of  $\LangSfive$  as its language, $\IS$   as its class of models, 
the satisfaction relation of Proposition~\ref{def:subjform} and the 
ordering of Definition~\ref{def:degofkn}. We will denote 
preferential entailment (as defined in 
Definition~\ref{def:preflog}) of Ground S5 by $\peGrSf$.
\end{definition}


The reader can now check that, for instance,  $Kp \peGrSf 
\neg Kq$. The (unique) minimal S5 model of  $Kp$  consists of all 
propositional valuations in which  $p$  is true, and this indeed 
contains a model in which  $q$  is false. The entailment relation is 
nonmonotonic since  $Kp \land Kq \not\peGrSf \neg Kq$. Another 
example illustrates the minimality of the agent's knowledge: $Kp \lor 
Kq \peGrSf \neg (Kp \land Kq)$.

Let us define a consequence relation  $\nminfrel$  by  $\phi 
\nminfrel \psi$  if  $K\phi \peGrSf K\psi$. Then it turns out that
this is the 
consequence relation of \citeauthor{HM85} \citeyear{HM85}, apart from the 
fact that they only defined it for premises which have a unique 
minimal model. Premises with a unique minimal model are called {\em honest}.  
To give an example,
the formula  $Kp$  is honest, but  $Kp \lor Kq$  is not: both 
the S5 model consisting of all valuations in which  $p$  is true, and 
the model with all valuations in which  $q$  is true, are minimal 
models.


\subsection{Minimal Temporal Epistemic Logic}

In Ground S5, we are only able to express something about `all the agent 
knows' at a particular instant. We will extend this logic in such a
way that we 
are also able to say something about the changing knowledge of the agent 
over time. Originally, this extended logic was intended as a means of 
specifying nonmonotonic reasoning processes and of reasoning 
about their properties 
\cite{ET94,ET96,En96a}. 
The idea is that a temporal formula describes the nonmonotonic 
inferences the agent has to perform during the course of a reasoning 
process (analogously to the use of temporal logic for specifying 
computer processes). But these inferences should also be the {\em 
only} cause of increases in the agent's knowledge. Therefore, we 
again have to minimize the agent's knowledge, but now over time 
\cite<analogously to the use of minimization for dealing with the frame 
problem in temporal logics for describing action and change,>{Sh88}. 
To this end, we will temporalize the epistemic 
language, epistemic models and the degree-of-knowledge ordering.

In order to describe past and future we introduce temporal 
operators  $P, H, F, G$  and  $\Box$, denoting respectively  
``sometimes in the 
past'', ``always in the past'', ``sometimes in the future'', ``always in 
the future''  and ``always''. We do not want to describe 
the agent's knowledge of the future and past, but the future 
and past of the agent's knowledge. Therefore, temporal operators 
are not allowed to occur within the scope of the epistemic  $K$  operator.

\begin{definition}[Temporal epistemic language]
The language  $\LangTEL$  is the smallest set closed under:
\begin{itemize}
\item if  $\phi \in \LangSfive$  then  $\phi \in \LangTEL$;
\item if  $\alpha, \beta \in \LangTEL$  then  $\alpha \land \beta, 
\neg \alpha, P\alpha, F\alpha \in \LangTEL$.
\end{itemize}
Again the abbreviations for  $\lor,  \to, \top$  and  $\bot$  are 
introduced,  as well as:
\[
G\alpha \equiv \neg F(\neg \alpha),  H\alpha \equiv \neg P(\neg 
\alpha)  \mbox{ and }  \Box\alpha \equiv H\alpha \land \alpha \land 
G\alpha.
\]
If in the first clause we restrict ourselves to subjective formulae, 
we get the set of {\em subjective TEL formulae}. 
\end{definition}


In the rest of this paper we will be interested in subjective TEL 
formulae since they describe how the knowledge of the agent is 
changing over time. Based on the set of natural numbers ($\nn$) as flow of 
time, and normal S5 models as formalization of states in a temporal 
model, the following semantics is introduced for temporal epistemic 
logic (TEL):

\begin{definition}[Semantics of TEL]\label{def:semtel}
A  TEL model is a function  $\telM : \nn \to \IS$ . The truth of a 
formula  $\phi \in \LangTEL$  in  $\telM$  at time point  $t \in 
\nn$, denoted  $( \telM , t) \models \phi$, is defined inductively 
as follows:
\[
\begin{array}{llll}
1. &  ( \telM , t) \models \phi & \Iff & \telM(t) \Sfsat \phi\mbox{, if 
} \phi \in \LangSfive \\
2. &  ( \telM , t) \models \phi \land \psi & \Iff & ( \telM , t) \models 
\phi \mbox{ and } (\telM , t) \models \psi \\
3. &  ( \telM , t) \models \neg \phi  &  \Iff  & \mbox{it is not the case 
that } ( \telM , t) \models \phi \\
4. &  ( \telM , t) \models P\phi  &  \Iff  &  \exists  s \in \nn \mbox{ 
such that } s < t  \mbox{ and  } ( \telM , s) \models \phi \\
5.  &  ( \telM , t) \models F\phi  &  \Iff  &  \exists s \in \nn \mbox{ 
such that } t < s  \mbox{ and } ( \telM , s) \models \phi
\end{array}
\]
A formula  $\phi$  is true in a model  $\telM$ , denoted  $\telM 
\models \phi$,  if  $( \telM , 0) \models \phi$. A TEL model  
$\telM$  is called {\em conservative}  (or {\em a TELC model}) 
if for all  $s < t \in \nn:   \telM (s) \prefto \telM (t)$, with the 
ordering  $\prefto$  of Definition ~\ref{def:degofkn}. The set of 
TELC models is denoted by  $\TCIS$. 
\end{definition}

Note that the above definition is in principle ambiguous: a formula
like $Kp \land Kq$ is an S5 formula which can be interpreted according
to the first semantic clause, but it can also be seen as a
conjunction, to be interpreted according to the second clause. As the
interpretation of the conjunction (and the same holds for negation) is
the same in S5 as in TEL, this ambiguity is harmless.

We will briefly explain the reason we have defined 
$\telM \models \phi$  if  $( \telM , 0) 
\models \phi$. Later on, we will make the general 
assumption on preferential logics that the language contains 
negation, and that  $m \satisf \neg \phi$  if and only if  $m \not\models  \phi$ 
(Assumption~\ref{ass:undlog}). If we define  $\telM \models \phi$  
if  $( \telM , t) \models \phi$  for all  $t \in \nn$, then this 
assumption would not hold for TEL. The two definitions can be 
translated into each other, since $( \telM , 0) \models \phi$  if and only if  $( 
\telM , t) \models \neg P\top \to \phi$  for all $t \in \nn$  and  $( \telM 
, t) \models \phi$  for all  $t \in \nn$  if and only if $( \telM , 0)  \models \phi 
\land G \phi$. This is also one of the reasons we gave a slightly different 
presentation of Ground S5 (using subjective formulae).

In conservative models, the propositional knowledge of an 
agent can only increase in time. We will restrict ourselves to these 
models, i.e., an agent can not forget or revise its 
(propositional) knowledge. Indeed, for a propositional formula  
$\phi$  and a TELC model  $\telM$ , if  $( \telM , t) \models K\phi$  
then  $( \telM , s) \models K\phi$  for all  $s > t$. This restriction can 
be made when the agent is reasoning about a fixed (non-changing) 
situation, and we are abstracting from particular implementation 
details (such as the use of backtracking implementations for 
nonmonotonic logics). We now extend the ordering and minimal 
consequence relation to TELC models. The ordering is extended in a 
pointwise fashion.

\begin{definition}[Minimal temporal epistemic logic]~
\begin{enumerate}
\item  We extend the degree-of-knowledge ordering to TELC models 
by defining
\[
\telM \prefto \telN  \Iff  \mbox{ for all }  s \in \nn:  \telM (s) \prefto 
\telN (s).
\]
\item  Minimal temporal epistemic logic (MTEL) is the 
preferential logic with the subjective TEL formulae as its 
language, $\TCIS$ as its class of models, the satisfaction relation  
($\telM \models \phi$) of Definition~\ref{def:semtel} and the 
ordering of item 1. We will denote preferential entailment (as 
defined in Definition~\ref{def:preflog}) of MTEL by 
$\peMTEL$.
\end{enumerate}
\end{definition}


The idea behind using MTEL for specifying reasoning processes is 
that a subjective TEL formula  $\phi$  describes the reasoning of an 
agent over time (it can, for example, describe the use of 
nonmonotonic inference 
rules, see Proposition~\ref{prop:dlintel}). 
The minimal models of  $\phi$  represent the process of the 
agent reasoning in time. We can then use minimal consequence to 
infer properties of this reasoning process. 

It is easy to see that MTEL is a generalization of Ground S5: for 
subjective S5 formulae  $\phi, \psi$  we have that $\phi \peMTEL 
\psi$  if and only if  $\phi \peGrSf \psi$. As an example of the use of 
the notion of minimal temporal epistemic consequence, it has been 
shown by  \citeauthor{ET93} \citeyear{ET93} that it can capture default logic 
\cite{Re80a}.

\begin{proposition}[Default logic in MTEL]
\label{prop:dlintel}
Let a finite, propositional default theory  $\Delta = \langle W, D 
\rangle$ be given and let  
\[
\psi = \bigwedge \{ \Box(K\alpha \land G(\neg K\neg \beta) \to 
G(K\gamma)) \mid (\alpha, \beta) / \gamma \in D \}  \land  \bigwedge \{ 
K\alpha \mid \alpha \in W \}.
\]
Then  $\phi$  is a sceptical consequence of  $\Delta$  in default 
logic if and only if  $\psi \peMTEL F(K\phi)$.
\end{proposition}

The conjuncts of the form  $\Box(K\alpha \land G(\neg K\neg \beta) 
\to G(K\gamma))$  ensure the application of the default rules. In
words: if the 
agent knows the prerequisite ($\alpha$), and the justification 
($\beta$) remains consistent with what the agent knows throughout 
the future, then the agent must conclude the consequent ($\gamma$) 
in the next moment in time (and it will know $\gamma$   
henceforth).


\subsection{Circumscription}

One of the earliest approaches to nonmonotonic reasoning is 
circumscription \cite{Mc77,Mc80,Da80,Li94,Et88}, 
a preferential logic based on first-order 
predicate logic. The main idea behind circumscription is a kind 
of completeness of information given to us: ``the premises as stated 
give us `the whole truth' about the matter'' \cite{Be89}. This leads 
to at least two kinds of minimality: predicate-minimality and 
domain-minimality. The intuition behind predicate-minimality is that 
for some relevant property (predicate), all objects that have this 
property, are explicitly said to have this property in the premise. This 
allows us to formulate defaults stating that all normal objects 
have some property. Minimizing abnormality will allow us to 
conclude an object has this property, unless we can deduce from 
the premise that this object is abnormal. The intuition behind 
domain-minimality, is that the domain (of discourse) contains no 
other objects than those that can be deduced to exist from the 
premise. 
\cite<This intuition is strongly tied to the domain-closure 
assumption of>{Re80b}.
These two kinds of minimality are formalized by two variants of 
Circumscription. Both of them  will be treated below.

The classical logic underlying circumscription is first-order 
predicate logic. We assume a standard first-order language 
$\Lang$ with a 
finite number of predicate symbols, including equality. We will also 
assume that the language contains no function or constant symbols. 
This is not a severe limitation, since we can eliminate function and 
constant symbols by introducing new predicate symbols 
\cite{Da80}. We will first give the definition of the orderings and 
then define predicate and domain circumscriptive consequence.

\begin{definition}~
\begin{enumerate}
\item  Let  $P$  be a predicate symbol in the language $\Lang$. For a 
structure  $M$  for the language, $P^M$  denotes the interpretation 
of  $P$  in  $M$  (so  $P^M$  is a subset of $dom(M)^n$, where 
$dom(M)$  is the domain of  $M$, and  $n$  is the arity of  $P$). 
For two structures $M, N$, we say  $M$  is  {\em $P$-preferred} 
to  $N$, denoted  $M \preftopred{P} N$, if they have the same 
domain, the same interpretation of predicate symbols other than  
$P$, and $P^M \subseteq P^N$. Predicate circumscription of  $P$  
is the preferential logic which uses first-order predicate logic for 
the language, models and satisfaction relation, augmented with 
the ordering  $\preftopred{P}$. We will denote preferential 
entailment (as defined in Definition~\ref{def:preflog}) in this 
logic by $\pePCirc{P}$.
\item  For two structures  $M, N$  for the language $\Lang$, we say  $N$  
is a {\em substructure} of  $M$, denoted  $N \preftodom M$,  if 
the domain of  $N$  is a subset of the domain of  $M$, and the 
interpretation of each predicate symbol in  $N$  is the restriction 
of the corresponding interpretation in  $M$  to  $dom(N)$. 
Domain circumscription is the preferential logic which uses first-order 
predicate logic for the language, models and satisfaction 
relation, augmented with the ordering  $\preftodom$. We will 
denote preferential entailment in this logic by  $\peDCirc$.
\item  If we restrict the model class to finite structures, the 
resulting preferential logics are called {\em finite predicate 
circumscription}  and {\em finite domain circumscription}. 
\end{enumerate}
\end{definition}


We refer the reader to the references given above
for standard results and motivation of circumscription.


\section{Respecting Monotonicity}\label{sec:respmon}

In this section we will study formulae which respect monotonicity. 
We will first give a formal definition.
\begin{definition}[Respecting monotonicity]
Given a preferential logic, we say a formula  $\phi$  {\em 
respects monotonicity}, if
\[
\forall\alpha, \beta:  \alpha \prefent \beta   \Implies  \alpha \land 
\phi \prefent \beta.
\]
\end{definition}

Next, we will make some basic assumptions about
the (underlying logic of the) preferential logic.

\begin{assumption}\label{ass:undlog}
>From now on we will assume that any preferential logic satisfies
the following:
\begin{itemize}
\item  the language has conjunction ($\land$) and  $m \satisf \phi
\land \psi  \Iff m \satisf \phi$  and  $m \satisf \psi$.
\item  the language has implication ($\to$) and  $m \satisf \phi \to
\psi  \Iff  m \not\satisf \phi$  or  $m \satisf \psi$.
\item  the language has negation ($\neg$) and  $m \satisf \neg \phi
\Iff  m \not\satisf \phi$.
\end{itemize}
\end{assumption}

We can then immediately identify a class of formulae that respect 
monotonicity:

\begin{proposition}\label{prop:dpimplmon}
Downward persistent formulae respect monotonicity.
\end{proposition}
\bproof
Suppose  $\phi$  is downward persistent. Let  $\alpha, \beta$  be 
formulae and suppose  $\alpha \prefent \beta$. Let  $m$  be a 
minimal model of  $\alpha \land \phi$. Then it is also a minimal 
model of  $\alpha$. For suppose it is not, then there exists  $n 
\prefto m$,  $n \neq m$  and  $n \satisf \alpha$. Since  $m \satisf 
\phi$  and  $\phi$  is downward persistent, we have  $n \satisf 
\phi$. But then  $n \satisf \alpha \land \phi$  which contradicts 
the assumption that  $m$  was a minimal model of  $\alpha \land 
\phi$. Since  $m$   is a minimal model of  $\alpha$  and  $\alpha 
\prefent \beta$, we have  $m \satisf \beta$. We have proved that  
$\alpha \land \phi \prefent \beta$. Thus,  $\phi$  respects 
monotonicity.
\eproof

Of course, valid and unsatisfiable sentences are downward 
persistent. But the question is whether non-trivial downward 
persistent formulae exist. For the preferential logics introduced in 
Section~\ref{sec:preflogs}, the answer is affirmative.

\begin{definition}[DIAM]\label{def:diam} 
Define the class of S5 formulae  $\DIAM$  by:
\[
\DIAM ::= M(\phi) \mid \DIAM \land \DIAM \mid \DIAM \lor \DIAM 
\mid M(\DIAM)
\]
where  $\phi$  is propositional. 
\end{definition}

Formulae from \DIAM\ essentially only contain the $M$ operator (the
`diamond' of S5, and not the `box' operator $K$).
Formulae in this class are the {\em only} 
subjective formulae (up to equivalence) which are downward 
persistent in Ground S5 \cite<this was proved by>{En96a}.

\begin{theorem}
A subjective S5 formula  $\phi$  is downward persistent in 
Ground S5 if and only if it is S5-equivalent to a formula in  
$\DIAM$.
\end{theorem}

So in Ground S5 there is a non-empty class of downward persistent 
formulae, that respect monotonicity by 
Proposition~\ref{prop:dpimplmon}. Essentially, these formulae only 
say something about the ignorance of the agent. One might think that 
formulae from  $\DIAM$ are completely uninteresting, and never 
yield any new insights in Ground S5. The converse of monotonicity 
for these formulae, $\alpha \land \phi \peGrSf \beta   \Implies   \alpha 
\peGrSf \beta$, however, does not hold, even when  $\phi$  is 
consistent with  $\alpha$. We do not have that  $Kp \lor Kq \peGrSf 
Kq$, whereas we do have that  $(Kp \lor Kq) \land M( \neg p) \peGrSf 
Kq$  with  $M( \neg p) \in \DIAM$. So knowledge of ignorance can be 
useful.

An analogous result holds for  minimal temporal epistemic 
logic.
\begin{definition}[TD]\label{def:td}~
\begin{enumerate}
\item Define
\[
\TD ::= \DIAM \mid \TD \land \TD  \mid \TD \lor \TD  \mid F(\TD)  
\mid G(\TD)  \mid P(\TD)  \mid H(\TD)
\]
\item For two subjective TEL formulae  $\phi, \psi$:
\[
\phi \sim \psi   \Iff_{def}   \mbox{ for all TELC models } \telM :  
\telM \models \phi \Iff \telM \models \psi.
\]
\end{enumerate}
\end{definition}


\TD\ stands for `temporal diamond' formulae. The following was also
proved by \citeauthor{En96a} \citeyear{En96a}.

\begin{theorem}
In MTEL, a formula  $\phi$  is downward persistent if and 
only if it is equivalent (in the sense of  $\sim$) to a formula in  
$\TD$.
\end{theorem}

As in the case of Ground S5, these formulae express (temporal) 
ignorance of the agent. 

\begin{definition}[Positive and universal 
formulae]\label{def:posuni} 
A first-order predicate formula is {\em negative in} a predicate  
$P$, if all occurrences of the predicate  $P$  are in the scope of an 
odd number of negations. A formula is {\em universal} if it is of 
the form $\forall x_1   \ldots   x_n \psi$  where  $\psi$  is quantifier 
free. 
\end{definition}


The following result links these formulae to downward persistence in 
circumscription. The first is a variant of Lyndon's theorem and is 
folklore (we leave the details to the reader); the second result is 
known as the {\L}o\'{s}-Tarski theorem 
\cite[Theorem 3.2.2]{CK90}.

\begin{theorem}~
\begin{enumerate}
\item  A first-order predicate formula  $\phi$  is downward 
persistent in predicate circumscription (of  $P$)  if and only if it 
is equivalent to a formula that is negative in  $P$.
\item  A first-order predicate formula  $\phi$  is downward 
persistent in domain circumscription if and only if it is equivalent 
to a universal formula.
\end{enumerate}
\end{theorem}

So downward persistent formulae in predicate circumscription 
essentially only say something about elements not having property  
$P$  (besides the other properties they mention), and downward 
persistent formulae in domain circumscription essentially only 
mention universal properties (and do not say anything about the 
existence of objects).

For our examples, we have shown that non-trivial classes of 
formulae that respect monotonicity exist. The question is whether 
there are more such formulae, besides those that are downward 
persistent. We will give a criterion that ensures that there are no 
more formulae that respect monotonicity.

\begin{definition}[Expressibility of preference]
A preferential logic satisfies {\em expressibility of preference} if 
the following holds:
\[
\forall m \in \Mod : \exists \phi^m \in \Lang: \forall n \in \Mod :  ( n 
\satisf \phi^m   \Iff  m \prefto n ).
\]
\end{definition}


The formula  $\phi^m$  expresses: ``I am less preferred than  $m$,'' 
and describes exactly those models which are larger in the 
preferential ordering. The criterion of expressibility of preference 
poses a requirement on the expressiveness of the language, given its 
semantics. We will prove that in preferential logics that satisfy the 
condition in this definition, the downward persistent formulae are the 
only ones that respect monotonicity. The above condition can be 
generalized by taking into account equivalent models; we have not 
done this immediately as it makes things rather cumbersome. If 
whenever  $n \prefto m$  and  $m \equiv k$  (where  $m \equiv k$  
means that   $m$  and  $k$  satisfy the same formulae), there exists a 
model  $l$  such that  $l \equiv n$  and  $l \prefto k$, then we can 
generalize the condition to: $\forall m \in \Mod : \exists \phi^m \in 
\Lang: \forall n \in \Mod :  ( n \satisf \phi^m   \Iff  \exists k \in \Mod: m 
\equiv k \;\&\; k \prefto n )$. 


\begin{theorem}[Only if \ldots]\label{th:oione}  
For a preferential logic that satisfies expressibility of preference 
we have:
if a formula respect monotonicity, then it is downward persistent.
\end{theorem}
\bproof
Suppose a formula  $\phi$  is not downward persistent, then 
there exist models  $m$  and  $n$  such that  $m \satisf \phi$,  $n 
\not\satisf \phi$  and  $n \prefto m$. Define  $\alpha = \phi^n \land 
( \phi \to \phi^m )$  and  $\beta = \neg \phi$. First we claim that  
$\alpha \prefent \beta$. Since  $n \prefto n$, we have  $n \satisf 
\phi^n$, and as  $n \not\satisf \phi$  we get  $n \satisf \alpha$. 
Furthermore, for any model  $k$, if  $k \satisf \alpha$  then in 
particular  $k \satisf \phi^n$  so  $n \prefto k$. Therefore,  $n$  is 
the only minimal model of  $\alpha$, and since  $n \not\satisf 
\phi$, we have  $n \satisf \beta$. On the other hand,  $\alpha \land 
\phi \not\prefent \beta$:  $n \prefto m$  so  $m \satisf \phi^n$  and  
$m \prefto m$  so $m \satisf \phi^m$  from which we conclude 
that  $m \satisf \alpha$  so  $m \satisf \alpha \land \phi$. 
Furthermore, for any model $k$, if  $k \satisf \alpha \land \phi$, 
then  $k \satisf \phi$  and  $k \satisf \phi \to \phi^m$  so  $k \satisf 
\phi^m$. From this it follows that  $m \prefto k$, but this means 
that  $m$  is a (actually, the only) minimal model of  $\alpha 
\land \phi$  and  $m \satisf \phi$  so  $m \not\satisf \beta$.  We 
conclude that  $\phi$  does not respect monotonicity, since we 
have found formulae  $\alpha$  and  $\beta$  such that  $\alpha 
\prefent \beta$  but  $\alpha \land \phi \not\prefent \beta$.
\eproof

It may seem that the condition of expressibility of preference is too 
restrictive. However, we will see that it is useful for the examples.

\begin{proposition}\label{prop:onlygmc}
For Ground S5, MTEL and finite predicate and domain 
circumscription, only downward persistent formulae respect 
monotonicity.
\end{proposition}
\bproof
Remark that all of these logics satisfy 
Assumption~\ref{ass:undlog}. First consider Ground S5. Let us 
first take the language to be finite (that is, $P$  is finite). Take 
any S5 model  $M$. 
For each propositional valuation  $m$, define the 
formula  $\alpha^m$  by  $\alpha^m = \bigwedge \{ p \in P \mid m 
\satisf p \} \land \bigwedge \{ \neg p \mid p \in P, m \not\models p 
\}$. This is a well-defined formula since  $P$  is finite. Now 
construct  $\phi^M = \bigwedge \{ K(\neg \alpha^m ) \mid m \notin M \}$, 
which is again a well-defined formula since $Mod(P)$  is finite. It 
can easily be seen that any S5 model  $N$  satisfies  $\phi^M$  if 
and only if  $M \prefto N$. So expressibility of preference is 
satisfied, whence Theorem~\ref{th:oione} ensures that only 
downward persistent formulae respect monotonicity for this 
finite language. Now let  $P$  be arbitrary, and suppose  $\phi$  
in this language respects monotonicity. Then it is easy to see that 
if we restrict the language to atoms occurring in  $\phi$, it still 
respects monotonicity, so it is downward persistent in the 
restricted language. It follows easily that  $\phi$  is also 
downward persistent in the full language.

For MTEL, the same considerations make it sufficient to give a 
formula  $\phi^{\telM}$   for a finite language only, so let us take  
$P$  finite. Then every S5 model  $\telM(i)$  is a finite set of 
propositional valuations. Since the sequence  $\{ \telM (i) \}$  is 
decreasing with respect to set-inclusion (as  $\telM$  is 
conservative), there will be an index  $k$  such that  $\telM (j) = 
\telM(k)$  for all  $j > k$. To improve readability of the formula  
$\phi^{\telM}$   we define the formulae  $at_i$  to be  $P^i \top 
\land H^{i+1} \bot$ (where  $P^i$  stands for a sequence of  $P$  
operators of length  $i$). It is easy to see that for any model  
$\telN$  we have  $(\telN , j) \models at_i$  if and only if  $j = i$. Now 
define: \\
$\phi^{\telM}  = \bigwedge \{ \Box( at_i  \to \phi^{\telM (i)} )  
\mid  0 \leq i \leq k \}$, where $\phi^{\telM (i)}$ is the formula as 
defined in the case of Ground S5 for the S5 model  $\telM (i)$ . It 
is easy to show that  $\telN \models \phi^{\telM}$ if and only 
if  $\telM \prefto \telN$.

For finite circumscription, we need the more general definition 
of expressibility of preference hinted at before 
(in first-order logic, there may be equivalent models: different
models that satisfy the same first-order formulae).
Here we need not restrict the 
language. In predicate circumscription, the required formula  
$\phi^M$  for a finite structure  $M$  expresses:  (i) the exact 
number of elements of the domain of  $M$,  (ii) for which of 
these elements  $P$  holds, and (iii)  for all other predicates  $Q$  
it expresses for which elements  $Q$  holds, and for which its 
negation holds. In domain circumscription, the required formula 
$\phi^M$  for a finite structure  $M$  expresses the fact that there 
are (at least) as many elements as in  $M$, and for each predicate  
$Q$, it expresses for which of these elements  $Q$  holds, and for 
which elements its negation holds.
\eproof

It is not possible to find the required formula  $\phi^M$  in 
(non-finite) circumscription in general: for infinite structures we are not in 
general able to express the number of elements, and we can not 
describe the entire extensions of predicates in general. Indeed, the 
above result does not hold for domain circumscription. It is still an
open question
whether it holds for predicate circumscription.

\begin{proposition}\label{prop:dcnoimpl}
For domain circumscription, there exists a first-order predicate 
formula which respects monotonicity but is not downward 
persistent.
\end{proposition}
\bproof
Consider the first-order language  $\Lang = \{<, =\}$, and let  
$\phi$  be a sentence stating that  $<$  is a dense linear ordering 
without begin- or endpoint. This is a complete theory 
\cite[Theorem 4]{Ra77}, which means that for any  $\alpha \in 
\Lang$, either  $\phi \models \alpha$  or  $\phi \models \neg 
\alpha$. Now suppose  $\alpha \peDCirc \beta$.  If  $\phi \models 
\neg \alpha$ then  $\alpha \land \phi$  is inconsistent, so  $\alpha 
\land \phi \peDCirc \beta$  trivially. Otherwise we have that  
$\phi \models \alpha$  so  $\alpha \land \phi$  is equivalent to  
$\phi$. But it is easy to see that  $\phi$  does not have a minimal 
model, so again we have $\alpha \land \phi  \peDCirc \beta$. 
However, $\phi$  is not downward persistent: it holds in the real 
numbers, but not in the substructure of the natural numbers.
\eproof

Until now we have considered formulae that can be added to any 
premise, but we can also ask the question whether a formula respects 
monotonicity for a given, fixed premise. 

\begin{proposition}\label{prop:crittwo}
Given a preferential logic such that  $\Mod$  is finite and for all  
$m \in \Mod$  there exists  $\alpha^m \in \Lang$  such that  $n 
\satisf \alpha^m$  if and only if  $n = m$, let $\alpha$ be a fixed formula
in $\Lang$. Then we have for all $\phi \in \Lang$:
\[
\forall \beta( \alpha \prefent \beta  \Implies  \alpha \land \phi 
\prefent \beta )  \Iff  \forall m \in \Mod( m \prefent \alpha \land \phi  
\Implies  m \prefent \alpha ).
\]
\end{proposition}
\bproof
The right to left direction is trivial (and does not depend on the 
assumption). For the other direction, suppose that  $\forall \beta( 
\alpha \prefent \beta  \Implies  \alpha \land \phi \prefent \beta )$. 
Let  $m \in \Mod$  be arbitrary and suppose  $m \prefent \alpha 
\land \phi$. Now define  $\beta = \bigvee \{ \alpha^n \mid n 
\prefent \alpha \}$; this is a well-defined formula since  $\Mod$  
was assumed finite. It is easy to see that  $\alpha \prefent \beta$: 
suppose  $n \prefent \alpha$, then  $\alpha^n$  is one of the 
disjuncts of  $\beta$, and by definition of $\alpha^n$, we have  $n 
\satisf \alpha^n$, so  $n \satisf \beta$. But the assumption now 
gives that  $\alpha \land \phi \prefent \beta$. As  $m \prefent 
\alpha \land \phi$, we have  $m \satisf \beta$, so there is an  $n \in 
\Mod$  with  $n \prefent \alpha$  and  $m \satisf \alpha^n$. But by 
definition of  $\alpha^n$  this means that  $m = n$  so  $m \prefent 
\alpha$.
\eproof

Proposition~\ref{prop:crittwo} states that a formula $\phi$ respects
monotonicity for a fixed premise $\alpha$ if and only if the minimal
models of $\alpha \land \phi$ are minimal models of $\alpha$.
Of course the criterion on the right-hand side is hard to check; we 
can give another criterion, but for that, we first need the following 
definition \cite{KLM90}:

\begin{definition}[Smoothness]
A preferential logic is called {\em smooth}, if the following 
holds:
\[
\forall \alpha \in  \Lang : \forall m \in \Mod: (m \satisf \alpha  
\Implies  \exists n \in \Mod: n \prefto m  \;\&\; n \prefent \alpha).
\]
\end{definition}


This condition, which is also called {\em stopperedness} or {\em 
well-foundedness}, and is akin to the {\em limit assumption} 
\cite{Le73}, forbids chains of ever-decreasing models satisfying a 
formula. It is one of the basic properties in the framework of 
\citeauthor{KLM90} \citeyear{KLM90}.

\begin{proposition}\label{prop:critthree}
Given a smooth preferential logic, we have: $\forall m \in \Mod( 
m \prefent \alpha \land \phi  \Implies  m \prefent \alpha )$  if and 
only if  $\forall m \in \Mod( m \satisf \alpha \land \phi  \Implies  
\exists n \in \Mod ( n \prefto m, n \prefent \alpha$  and  $n \satisf 
\phi ))$.
\end{proposition}

The proof of this proposition is straightforward, and again it may not 
help much. As far as the examples are concerned, the conclusion of 
Proposition~\ref{prop:crittwo} holds for both Ground S5 and MTEL 
(the properties depend only on  $\alpha$  and  $\phi$  so we may 
restrict the signature and then use the proposition). 
Proposition~\ref{prop:critthree} holds for Ground S5 (which is 
smooth). From these propositions we can find some sufficient 
conditions. If  $\phi$  is downward persistent in the models of  
$\alpha$, then Proposition~\ref{prop:crittwo} ensures that  $\phi$  
respects monotonicity with respect to  $\alpha$. If  $\alpha \prefent 
\phi$  then Proposition~\ref{prop:critthree} ensures that $\phi$  
respects monotonicity with respect to  $\alpha$  
\cite<but this also follows 
immediately with the rule of Cautious Monotonicity, which is 
satisfied in smooth preferential logics, >{KLM90}. 
It seems 
hard to find a simple criterion necessary and sufficient for respecting 
monotonicity for a given premise. We leave this for further research.


\section{Conservativity}\label{sec:cons}

In the previous section we have considered formulae that can always 
be added to a premise without invalidating any of the conclusions. In 
this section we will focus on the conclusions, and study formulae 
that, when they are concluded, can always be kept, no matter which 
new information is added to the premise. We will call these formulae 
conservative.

\begin{definition}[Conservative]
Given a preferential logic, we say a formula  $\beta$  is {\em 
conservative}, if
\[
\forall \alpha, \phi:  \alpha \prefent \beta   \Implies  \alpha \land 
\phi \prefent \beta.
\]
\end{definition}


We have the following result connecting upward persistent and 
conservative formulae, in analogy with 
Proposition~\ref{prop:dpimplmon}.

\begin{proposition}\label{prop:upimplcons}
Given a preferential logic that is smooth, if a formula is upward 
persistent, it is conservative.
\end{proposition}
\bproof
Let  $\beta$  be upward persistent in a smooth preferential logic. 
Now suppose  $\alpha \prefent \beta$ . Take any model  $m$  
such that  $m \prefent  \alpha \land \phi$, then  $m \satisf \alpha$  
so by smoothness, there is a model  $n$  with  $n \prefto m$  and  
$n \prefent \alpha$. Then, as  $\alpha \prefent \beta$, we have  $n 
\satisf \beta$. Since  $n \prefto m$  and  $\beta$  is upward 
persistent, we have  $m \satisf \beta$. This shows that $ \alpha 
\land \phi \prefent \beta$, so  $\beta$  is conservative.
\eproof

Again, we can ask if the upward persistent formulae are the only 
conservative formulae, and this is true under the same conditions as 
in the case of respecting monotonicity.
\begin{proposition}[Only if \ldots]\label{prop:oifour} 
For a preferential logic that satisfies expressibility of preference 
we have:
if a formula is conservative, then it is upward persistent.
\end{proposition}
\bproof
Suppose  $\beta$  is not upward persistent, then there are  $n, m 
\in \Mod$  such that  $n \prefto m$,  and $n \satisf \beta$  but  $m 
\not\satisf \beta$.  Now take  $\alpha = \phi^n$  and  $\phi = 
\phi^m$. Then  $n$  is the only minimal model of  $\alpha$  and  
$n \satisf \beta$  so  $\alpha \prefent \beta$, but  $m$ is a 
(actually, the only one) minimal model of  $\alpha \land \phi$, 
and  $m \not\satisf \beta$, so  $\alpha \land \phi \not\prefent 
\beta$. Thus,  $\beta$  is not conservative.
\eproof

Let us first identify the upward persistent formulae for our examples. 
This is relatively straightforward, since we have the following 
elementary result.

\begin{proposition}
For any preferential logic,  $\phi$  is upward persistent if and 
only if  $\neg \phi$  is downward persistent.
\end{proposition}

This gives us the following.

\begin{proposition}\label{def:boxtbposex}~
\begin{enumerate}
\item  Define  $\BOX ::= K(\phi) \mid \BOX \land \BOX \mid \BOX 
\lor \BOX \mid K(\BOX)$  with  $\phi$ propositional. Then a 
subjective S5 formula  $\phi$  is upward persistent in Ground S5 
if and only if it is S5-equivalent to a formula in  $\BOX$.
\item  Define  $\TB ::= \BOX \mid \TB \land \TB \mid \TB \lor \TB 
\mid F(\TB) \mid G(\TB) \mid P(\TB) \mid H(\TB)$. Then a 
subjective TEL formula  $\phi$  is upward persistent in MTEL if 
and only if it is equivalent (in the sense of  $\sim$) to a formula 
in  $\TB$.
\item  A first-order formula is upward persistent in predicate 
circumscription (of  $P$) if and only if it is equivalent to a 
formula that is positive in  $P$  (meaning that all occurrences of 
the predicate  $P$  are in the scope of an even number of 
negations). A first-order formula is upward persistent in domain 
circumscription if and only if it is equivalent to an existential 
formula (a formula of the form  $\exists x_1 \ldots x_n \psi$  
where  $\psi$  is quantifier free).
\end{enumerate}
\end{proposition}
\bproof
Straightforward.
\eproof

In the above definition, formulae from \BOX\ essentially only contain
the $K$ operator (the `box' of S5); \TB\ stands for
`temporal box' formulae.
Now let us see what Propositions \ref{prop:upimplcons} and 
~\ref{prop:oifour} say about the examples. Ground S5 satisfies 
expressibility of preference (for a finite language) and is smooth, so 
the conservative formulae are exactly the upward persistent 
formulae, which express only knowledge (and not ignorance). This 
can be lifted again to an infinite language. The fact that in Ground 
S5, formulae that express propositional knowledge, are conservative, 
was already noted by \citeauthor{DNR95} \citeyear{DNR95}. 
MTEL also satisfies 
expressibility of preference (for a finite language), so any formula 
that is conservative, must be upward persistent, and must be 
equivalent to a formula in $\TB$, expressing knowledge over time 
(not ignorance). This can be lifted to an infinite language. 
Unfortunately, MTEL is not smooth: the formula  $F(Kp)$  is 
satisfiable, but has no minimal model. In MTEL, we have that  
$F(Kp) \peMTEL F(Kq)$, but  $F(Kp) \land Kp \not\peMTEL F(Kq)$  
($F(Kp) \land Kp$  has a minimal model, in which only  $p$  is 
known, from the first point in time onwards). This means that the 
formula  $F(Kq)$  is not conservative, although it is upward 
persistent. It is easy to see that in any preferential logic, valid 
formulae are always conservative, but in MTEL, these are (almost) 
the only ones.

\begin{definition}
We call a TEL model  $\telM$  {\em totally ignorant}, if for all 
propositional formulae  $\phi$  we have: if  $\telM  \models 
F(K\phi)$  then  $\phi$  is a propositional tautology. Define {\em 
the totally ignorant model}  $\telMti$  by  $\telMti (i)  = Mod(P)$  
for all  $i$. 
\end{definition}


In a totally ignorant model, no knowledge is ever gained. {\em The} 
totally ignorant model is certainly {\em a} totally ignorant model, 
and if  $P$  is finite, it is the only one.

\begin{proposition}
For MTEL, in case  $P$  is infinite, we have that a formula is 
conservative if and only if it is true in all models. When  $P$  is 
finite, a formula is conservative if and only if it is true in all 
models except possibly the totally ignorant model.
\end{proposition}
\bproof
We will prove that  $\beta$  is conservative if and only if it is 
true in all models that are not totally ignorant (both when $P$ is
finite and when it is infinite). First, suppose  
$\telM$  is a model that is not totally ignorant, in which  $\beta$  
is not true. So  $\telM \models F(K\gamma)$  for some 
propositional formula  $\gamma$  that is not a propositional 
tautology. If $P$ is finite, we can consider the formula $\phi^{\telM}$
(see the proof of Proposition~\ref{prop:onlygmc}
for the definition of   $\phi^{\telM}$). If $P$ is infinite, one can
show that $\telM$ can be chosen in such a way that it is a `inherently
finite' model, allowing the construction of a formula $\phi^{\telM}$
with the same properties as for the case when $P$ is finite
(using essentially the same construction). The details of this
argument are left to the reader.
The formula  $F(K\gamma)$  does not have a minimal model 
($\gamma$  must be known sometimes in the future, but this 
moment can always be postponed, yielding a smaller model), so  
$F(K\gamma) \peMTEL \beta$. 
On the other hand, it can easily be 
shown that the only minimal model of  $F(K\gamma) \land 
\phi^{\telM}$   is  $\telM$ , which gives us  
$F(K\gamma) \land \phi^{\telM}  \not\peMTEL \beta$. This 
means that  $\beta$  is not conservative. 

Now suppose that  
$\beta$  is true in all models that are not totally ignorant, and 
suppose  $\alpha \peMTEL\beta$. Let  $\telM$  be a minimal 
model of  $\alpha \land \phi$. If  $\telM$  is not totally ignorant, 
then  $\telM \models \beta$. If it is totally ignorant, then also  
$\telMti \models \alpha \land \phi$ (it can be shown by induction that
all totally ignorant models satisfy the same formulae).
But then  $\telMti \models 
\alpha$. Since no model is preferred over  $\telMti$, this means 
that $\telMti \prefent \alpha$  so  $\telMti \models \beta$, 
whence  $\telM \models \beta$. It follows that  $\alpha \land \phi 
\peMTEL \beta$, so  $\beta$  is conservative. 

Let us look at 
the case when  $P$  is infinite. Suppose  $\telM \not\models 
\beta$, with  $\telM$   totally ignorant. Now take a propositional 
atom  $p$  not occurring in $\beta$. It can easily be shown that 
we can find a model of  $Kp$  in which  $\beta$  is not satisfied. 
This model is of course not totally ignorant. This shows that if  
$\beta$  is true in all models that are not totally ignorant, then it is 
true in all models. In case  $P$  is finite,  $\telMti$  is the only 
totally ignorant model.
\eproof

So in MTEL with an infinite  $P$, valid formulae are the only 
conservative formulae. These formulae are of course upward 
persistent (in a trivial way), and they are equivalent to a formula in  
$\TB$, for instance  $K(\top)$. When the signature is finite, there are 
some extra formulae that are conservative, for example if  $P = \{ p, q 
\}$, then the formula  $F(K(p \lor q) \lor K(\neg p \lor q) \lor K(p \lor 
\neg q) \lor K(\neg p \lor \neg q))$  is also conservative  (it is true in all 
models except the totally ignorant one). Of course, this formula is 
upward persistent, and it is in  $\TB$.

Finite predicate and domain circumscription satisfy both 
expressibility of preference and smoothness, so the conservative 
formulae coincide with the upward persistent formulae which have 
the syntactic characterization of Proposition~\ref{def:boxtbposex}.

Full circumscription satisfies neither of the conditions.

\begin{proposition}
In predicate and domain circumscription there are upward 
persistent formulae that are not conservative.
\end{proposition}
\bproof
First consider predicate circumscription. Let the language consist 
of three predicates besides equality, namely  $P$, $\Succ$  and
$<$
(and  $P$  is circumscribed). Define the formulae  $\alpha$  and  
$\phi$  as follows:
\[
\begin{array}{lll}
\alpha = & \forall x \exists ! y ( \Succ(x, y)) \land &  \phi = \forall
x y ( Px \land \Succ(y, x) \to Py)\\
	& \forall x \exists ! y ( \Succ(y, x)) \land  & \\
	& \forall x y ( \Succ(x, y) \to x < y ) \land & \\
 	& \forall x y z ( x < y \land y < z  \to x < z ) \land & \\
 	& \forall x ( \neg ( x < x ) ) \land & \\
 	& \forall x y ( x < y \lor y < x \lor x = y ) \land & \\
	& \exists x Px & \\
	& \forall xy ( Px \land \Succ(x, y) \to Py)
\end{array}
\]
The intuitive meaning of $\alpha$ is that there are $\Succ$-chains
of elements, extending indefinitely in both directions. If $P$ occurs
somewhere on such a chain, it must be true in all successors as well.
A model of $\alpha$ can be made smaller (more preferred) by making $P$
false in a point and all of its predecessors (leaving it true in all
successors). We will now make this argument formal.
The first claim is that  $\alpha$  has no  $\preftopred{P}$-
minimal models. Let  $M$  be a model of  $\alpha$. Then there 
must be an  $x \in dom(M) $ with  $x \in P^M$. Define  $A = \{ x \} 
\cup \{ y \in P^M  \mid (y, x) \in <^M \}$.
Let  $N$  be the 
structure with the same domain as  $M$, the same extension of  
$\Succ$ and $<$, and  $P^N = P^M \setminus A$. It is straightforward to 
verify that  $N$  is a model of  $\alpha$, and that  $N 
\preftopred{P} M$  and  $N \neq M$. 

On the other hand,  $\alpha \land \phi$  has minimal models. Let  
$M$  be the structure with  $dom(M) = \integers$  (the integers), 
$(a, b) \in \Succ^M  \Iff  b = a + 1$, $(a, b) \in <^M \Iff a < b$ in
the natural ordering on the integers, and  $P^M = \integers$. It can 
easily be checked that  $M \models \alpha \land \phi$. Now 
suppose  $N \preftopred{P} M$,  $N \neq M$  and  $N \models 
\alpha \land \phi$. This means that  $P^N \subset \integers$  
(strict inclusion), and  $P^N  \neq \emptyset$  (as  $N \models 
\exists x Px$). But then there must be  $x, y \in \integers$  with  $y 
= x + 1$, and either  $x \in P^N$  and  $y \notin P^N$,  or  $x \notin 
P^N$  and  $y \in P^N$, contradicting either  $N \models \forall x y 
( Px \land \Succ(x, y) \to Py$)  ($N \models \alpha$) or  $N \models 
\phi$. Therefore  $M$  is a minimal model of  $\alpha \land \phi$.

Now define  $\beta = \exists x ( x \neq x )$, which is trivially 
upward persistent. Since  $\alpha$  has no minimal models, we 
have  $\alpha \pePCirc{P} \beta$, but  $M \not\models \beta$, so  
$\alpha \land \phi \not\pePCirc{P} \beta$. This shows that  $\beta$  is 
not conservative.
\vspace{0.5cm}

For domain circumscription, the example is quite similar.
Again take  $\beta = \exists x ( x \neq x )$. Now define the 
formulae  $\alpha$  and  $\phi$  as follows:
\[
\begin{array}{lll}
\alpha = &\forall x \exists ! y ( \Succ(x, y)) \land & \phi = \forall 
y\exists x( \Succ(x, y) ) \\
 &	\forall x y ( \Succ(x, y) \to x < y ) \land & \\
 &	\forall x y z ( x < y \land y < z  \to x < z ) \land& \\
 &	\forall x ( \neg ( x < x ) ) \land& \\
 &	\forall x y ( x < y \lor y < x \lor x = y ) \land& \\
 &	\forall x y z ( \Succ(x, z) \land \Succ(y, z)  \to x = y )
\end{array}
\]
One can now check that  $\alpha$  has no  $\preftodom$-minimal 
models, but  $\alpha \land \phi$  does, so the same  $\beta$  is 
upward persistent but not conservative in domain 
circumscription. The details are left to the reader.
\eproof

Until now, we have looked at formulae which, once concluded, are 
never lost, regardless of what new information comes in, but also 
regardless of what the initial premise was. However, we can also 
consider the situation with the premise fixed (analogously to the last 
part of the previous section): given a premise, which conclusions 
may be kept regardless of new information?

\begin{proposition}\label{prop:epcrit}
For a preferential logic that satisfies expressibility of preference, 
if  \\
$\alpha \prefent \beta$, then
\[
( \forall \phi: \alpha \land \phi \prefent \beta )  \Iff   \alpha \models 
\beta.
\]
\end{proposition}
\bproof
Suppose  $\alpha \prefent \beta$. \\
``$\Leftarrow$'' If  $\alpha \models \beta$  then for any  $\phi$  
we have  $\alpha \land \phi \models\beta$  so  $\alpha \land \phi 
\prefent \beta$. \\
``$\Implies$''  Suppose  $\alpha \not\models \beta$, then there exists  
$m \in \Mod$  such that  $m \satisf \alpha$  but  $m \not\satisf 
\beta$. Then  $m \prefent  \alpha \land \phi^m$  (!), so  $\alpha 
\land \phi^m \not\prefent \beta$.
\eproof

Note that the condition  $\alpha \prefent \beta$  was not used in the 
proof; if  $\alpha \not\prefent \beta$  the equivalence is still true, as 
both sides are false. The proposition shows that the monotonic 
consequences of a premise are the only ones conservative with 
respect to this fixed premise.

\begin{corollary} \label{cor:epcrittwo}
Let  $\beta$  be a conservative formula for a preferential logic 
that satisfies expressibility of preference, then  $\alpha \prefent 
\beta  \Iff  \alpha \models \beta$.
\end{corollary} 
\bproof
If  $\alpha \models \beta$  then in any preferential logic it follows 
that $\alpha \prefent \beta$. On the other hand, if  $\alpha \prefent 
\beta$ , then for any  $\phi$  we have  $\alpha \land \phi \prefent 
\beta$ , since  $\beta$  is conservative. With 
Proposition~\ref{prop:epcrit} it follows that  $\alpha \models 
\beta$.
\eproof

In the last two sections, we have derived a number of results on 
formulae that respect monotonicity and conservative formulae and 
the links with persistent formulae. In the next section we will discuss 
the impact of these results in practice.


\section{Practical Implications}\label{sec:pracimpl}

The results in this paper may improve the efficiency of theorem 
provers for preferential logics, depending on a number of factors. In 
the first place, it is important how the theorem prover is used.

Consider the situation where we have a stand-alone theorem 
prover which gets different (unrelated) queries. Furthermore,
suppose the theorem prover is asked to prove 
$\alpha_1 \land \ldots \land \alpha_n \prefent \beta$. 
Then there are at
least two possibilities for using the results in the paper. First of
all, suppose the preferential logic satisfies expressibility of preference.
Then if $\beta$  is upward persistent, we do not
have to prove  $\alpha_1 \land \ldots \land \alpha_n \prefent
\beta$, as it is equivalent to prove  $\alpha_1 \land \ldots \land
\alpha_n \models \beta$ (Corollary~\ref{cor:epcrittwo}). In most
preferential logics, preferential entailment is harder to compute than
entailment in the underlying logic. 

In the second place, sometimes local reasoning is possible 
(which is not possible in general for 
non-monotonic logics): the theorem prover may derive the 
conclusion from part of the 
premise. So it may be the case that there is a  $1 \leq k < n$  
such that  $\alpha_1 \land \ldots \land \alpha_k \prefent 
\beta$  which is easier to verify than the original query. Then if  
$\alpha_{k+1} , \ldots , \alpha_n$  are downward persistent, 
Proposition~\ref{prop:dpimplmon} implies that  $\alpha_1 \land 
\ldots \land \alpha_n \prefent \beta$. If  $\beta$  is upward persistent 
(and the preferential logic is smooth), 
Proposition~\ref{prop:upimplcons} sanctions  $\alpha_1 \land \ldots 
\land \alpha_n \prefent \beta$. For these results to be usable in a 
theorem prover, we need heuristic knowledge to decide if there is a
promising split of the premise into two parts  $A$  and  $B$. For such
a split, we can then try to prove  $A \prefent \beta$  and 
downward persistence of  $B$  or upward persistence of  $\beta$.  In 
case  $\alpha_1 \land \ldots \land \alpha_k \prefent \beta$  can not be 
proved, we may have to directly prove  $\alpha_1 \land \ldots \land 
\alpha_n \prefent \beta$  after all. 

These two methods will of course only improve efficiency if the determination 
of persistence is easier than the original query (we will treat this 
question below).

The second kind of situation is when we have a theorem prover 
which is used by an agent which has a lot of knowledge about the 
world, and from time to time performs observations to increase its 
knowledge. Then, although sometimes the agent will need to 
perform revisions, we are often in the situation that (many) 
conclusions from a premise ($\alpha$) have been proved, and the 
premise is augmented by a new formula  ($\phi$). If this new 
formula is downward persistent, then the agent can retain all the old 
conclusions (and may only need to derive some new conclusions). If 
it is not, it can at least retain all the upward persistent conclusions (if 
the preferential logic is smooth). We may also try to determine if  
$\phi$  is downward persistent given  $\alpha$, or if  $\beta$  is 
conservative given  $\alpha$. Again, these methods only improve 
efficiency if it is easier to determine if  $\phi$  respects monotonicity 
(possibly given  $\alpha$) than recomputing all old conclusions, or if 
it is easier to determine that  $\beta$  is conservative (possibly given  
$\alpha$) than checking  $\alpha \land \phi \prefent \beta$.

The possible efficiency improvement in both cases heavily 
depends on the cost of determining persistence relative to the cost of 
determining preferential consequence. Unfortunately, it is very hard 
to say anything about this issue in general. It depends on the 
preferential logic at hand, on the representation of the logic 
(syntactically, as a proof calculus, or semantically, as models with a 
preference relation), and on other implementation issues. For 
instance, it can be important how much information is retained from 
previous queries: whether proofs or minimal models are stored.
Let us consider the examples again.

Preferential entailment in both Ground S5 and MTEL is  
$\prod_3^P$-complete \cite{En96a}, whereas full circumscription 
is undecidable (restricted versions of circumscription exist which are 
decidable, but still highly complex). Unfortunately, determining 
downward or upward persistence is not easier for these logics. We 
have seen that the classes of persistent formulae have syntactic 
representations of the form:  $\phi$  is upward/downward persistent 
if and only if it is equivalent to a formula in  $C$, where  $C$  is a 
(syntactic) class of formulae. Now, of course, determining 
{\em equivalence to} a formula in  $C$  is as complex as determining 
persistence, but there may be subclasses of a class of persistent 
formulae, with a lower complexity. For instance, determining {\em 
membership} of  $C$  is much easier, namely polynomial. The 
members of  $C$  are persistent. So what we propose is to check 
membership of $C$, instead of equivalence to a member of  $C$. In that 
case, we will miss some persistent formulae (and have to prove the 
original query), but this disadvantage is outweighed by the 
complexity advantage of checking membership. The checking of 
membership can be improved upon by adding some (easy) checks 
for equivalence to a formula in  $C$. For instance, in Ground S5, if 
we consider, for a formula  $\phi$, for each propositional 
sub-formula, the nearest  $K$  operator in which scope it lies, then if 
all of these  $K$  operators are in the scope of an odd number of 
negations, we can conclude that  $\phi$  is downward persistent. The 
formula  $\neg K( q \lor Kp )$, for example, satisfies this condition, 
and although it is not a member of  $\DIAM$, it is equivalent to  
$\neg Kq \land \neg Kp \in \DIAM$. This check is obviously 
polynomial.

Given a preferential logic, the designer of a theorem prover could 
proceed as follows. First, syntactic classes of formulae that are 
downward and upward persistent have to be identified. For Ground 
S5, MTEL and predicate and domain circumscription, these can be 
found in Definitions \ref{def:diam}, \ref{def:td}, 
\ref{def:posuni} and Proposition~\ref{def:boxtbposex}. For other 
preferential logics, if such classes are trivial (they may, for instance, 
only include tautologies and contradictions), then the 
usefulness of the results is limited. Otherwise, the theorem prover 
could work as follows. Given a query of the form  $\alpha \land \phi 
\prefent \beta$, first it is checked if  $\phi$  belongs to the syntactic 
class of downward persistent formulae or if  $\beta$   belongs to the 
syntactic class of upward persistent formulae (this latter test should 
only be performed if the preferential logic is smooth). If  $\beta$  is 
conservative and the logic satisfies expressibility of preference, it 
tries to prove $\alpha \land \phi \models \beta$  
\cite<this usually has a 
lower complexity than the original query; for Ground S5 and MTEL, 
monotonic consequence is NP-complete, >{En96a}. 
The answer of this query is the answer to the original query (see 
Corollary~\ref{cor:epcrittwo}). Otherwise, if $\phi$  belongs to the 
syntactic class of downward persistent formulae or if  $\beta$   
belongs to the syntactic class of upward persistent formulae (but the 
logic does not satisfy expressibility of preference), then the theorem 
prover tries to prove $\alpha \prefent \beta$. If this succeeds, it 
outputs yes. Otherwise, it will try to answer the original query 
directly.

As stated before, the practical savings in part depend on 
representation and implementation aspects. It also depends on the 
application domain and use of the theorem prover: if formulae in 
these syntactic classes occur often, the efficiency improvement is 
higher than if they are infrequent.


\section{Conclusions and Further 
Research}\label{sec:concl}

We have looked at restrictions of monotonicity in preferential logics. 
While monotonicity does not hold in general, we can identify (in 
general non-trivial) classes of formulae for which restricted versions 
of monotonicity holds. This may make (nonmonotonic) deduction in 
preferential logics easier, since we may sometimes keep conclusions, 
or identify which conclusions may be kept, when adding new 
information to a premise. The results in this paper may lead to more 
efficient implementations of preferential logics. Experimenting with 
theorem provers which use these results is necessary in order to 
determine the efficiency improvement in practice.

It would be nice to find a better characterization of formulae that 
can be added to a given, fixed premise without destroying 
conclusions.

Syntactic characterizations of persistent formulae were given for 
a number of example preferential logics, but we would like to have a 
result for broader classes of preferential logics, such as the class of 
ground nonmonotonic modal logics \cite{DNR95}.


\acks{I would like to thank Riccardo Rosati for stimulating discussions and 
worthwhile suggestions. Also, I would like to thank Pascal van Eck, 
Jan Treur, Rineke Verbrugge, Elles de Vries and Wieke de Vries
for reading and commenting on 
earlier versions of this document. Furthermore, I would like to thank 
Heinrich Herre for suggesting the example in 
Proposition~\ref{prop:dcnoimpl}. The anonymous referees helped to 
improve the paper.}

\bibliographystyle{theapa}
\bibliography{DPMon}

\end{document}


