# Dual Forgetting Operators in the Context of Weakest Sufficient and Strongest
Necessary Conditions

Patrick Doherty 11footnotemark: 1222The first author has been partially
supported by a grant from the ELLIIT Network Organization for Information and
Communication Technology, Sweden, in addition to a research grant from
Mahasarakham University, Thailand<EMAIL_ADDRESS>Department of
Computer and Information Science
Linköping University, SE-581 83 Linköping, Sweden  Faculty of Informatics
Mahasarakham University, Mahasarakham, Thailand  Andrzej Szałas333The first
author has been partially supported by a grant from the ELLIIT Network
Organization for Information and Communication Technology, Sweden, in addition
to a research grant from Mahasarakham University, Thailand.444The second
author has been supported by grant 2017/27/B/ST6/02018 of the National Science
Centre Poland<EMAIL_ADDRESS>Institute of Informatics, University of
Warsaw
Banacha 2, 02-097 Warsaw, Poland

###### Abstract

Forgetting is an important concept in knowledge representation and automated
reasoning with widespread applications across a number of disciplines. A
standard forgetting operator, characterized in [26] in terms of model-
theoretic semantics and primarily focusing on the propositional case, opened
up a new research subarea. In this paper, a new operator called weak
forgetting, dual to standard forgetting, is introduced and both together are
shown to offer a new more uniform perspective on forgetting operators in
general. Both the weak and standard forgetting operators are characterized in
terms of entailment and inference, rather than a model theoretic semantics.
This naturally leads to a useful algorithmic perspective based on quantifier
elimination and the use of Ackermman’s Lemma and its fixpoint generalization.
The strong formal relationship between standard forgetting and strongest
necessary conditions and weak forgetting and weakest sufficient conditions is
also characterized quite naturally through the entailment-based, inferential
perspective used. The framework used to characterize the dual forgetting
operators is also generalized to the first-order case and includes useful
algorithms for computing first-order forgetting operators in special cases.
Practical examples are also included to show the importance of both weak and
standard forgetting in modeling and representation.

###### keywords:

Knowledge representation and Reasoning, Forgetting , Weakest Sufficient
Conditions , Strongest Necessary Conditions, Quantifier Elimination

††journal: arxiv.org

##  1 Introduction and Motivation

From a knowledge representation and automated reasoning perspective,
remembering is essentially what an agent system does when adding new logical
statements to a knowledge or belief base. Remembering, in this context, is a
powerful way of modeling and is the basis for decision making in many agent
systems. On the surface, remembering appears to be straightforward, simply add
a new statement to a knowledge or belief base. But what if one wants to retain
consistency or some other property of the knowledge or belief base upon
assertion of additional statements? The knowledge or belief base would then
need to be modified in various ways. Then the problem becomes more complex and
leads to different subareas in Knowledge Representation, such as belief
revision [3, 18, 29] or research with consistency preserving operators [3,
24].

This setting also leads naturally to the dual concept of forgetting. Given a
knowledge or belief base, what does it mean to forget parts of it permanently,
or temporarily for reasons of expedience? Here, on the surface also,
forgetting appears to be straightforward, simply remove a statement from a
knowledge or belief base. But, as in the case of remembering, there is a great
deal of subtlety and choice concerning why and how one might remove a
statement, or parts of statements from a knowledge or belief base.

The spectrum between explicit remembering and explicit forgetting and the
operators that would be needed for specifying the different degrees in
between, offer a complex set of research topics in Knowledge Representation.
Lin and Reiter [26] opened up a new subarea of Knowledge Representation with
the introduction of a (standard) forgetting operator applied to a knowledge or
belief base. The forgetting operator is specified in terms of model-theoretic
semantical criteria, as are its properties. The focus in their work is
primarily propositional, but there is consideration of the first-order case.
The basic question asked and answered is “what does it mean to forget certain
concepts (propositional variables) in a knowledge base and how does this
influence entailment of formulas in that knowledge base?”.

This context is the starting point for this paper. Here the interest is in
exploring whether there are other well-behaved forgetting operators in the
spectrum discussed above and how they may relate to the original standard
forgetting operator. Such operators should also be useful representationally
and pragmatically.

Consider the following motivating example where the need for an additional
forgeting operator is considered. Let $lt$ and $lp$ stand for “low
temperature” and “low pressure”, respectively. Assume we are modeling a
physical system and want to maintain the property:

$lt\lor lp.$ (1)

Consider a situation when a temperature sensor associated with the system is
broken and we receive no meaningful information about $lt$. To adapt the model
for this situation, we would then want to temporarily forget $lt$. According
to standard approaches of forgetting, this would result in the second-order
formula [26]:

$\exists\,lt\,\big{(}lt\lor lp\big{)}.$ (2)

Formula (2) is equivalent to true, so this would leave us empty-handed when
reasoning about maintaining (1) with the associated changes in the system. No
additional consequences of the change in the system can be derived. This
happens since standard forgetting has the property of preserving entailment
(see Proposition 10, point 2 in [26]), where one is interested in what a given
theory entails, i.e., in the necessary conditions of the theory. On the other
hand, in this situation one would expect that $lp$ itself should still be
maintained, as it is a sufficient condition for (1). However, this weaker from
of reasoning is not covered by standard forgetting.

Although this is a simple example, it allows us to target what this paper is
about. We are interested in this weaker form of reasoning associated with
forgetting and its relation to the stronger standard form of reasoning with
forgetting and how these two forms of forgetting can be used in various
applications.

The original contributions of the paper include:

  * 1.

complementing the standard forgetting operator with a new one, the weak
forgetting operator, that is dual to standard forgetting, useful in
applications and, surprisingly, not explicitly considered in the literature so
far;555In the paper, we call the new operator the weak forgetting operator and
the standard operator found in the literature, either the standard or the
strong forgetting operator.

  * 2.

specifying forgetting operators in a general, principled framework that is
directly related to entailment and inference rather than through a semantic
construction of model equivalence as is typically used in defining standard
forgetting (see, e.g., [26, Definition 1] and other related work);

  * 3.

the formal framework introduced shows the strong dual relationship between
standard forgetting and strongest necessary conditions, and weak forgetting
and weakest sufficient conditions. This relationship follows naturally from
the entailment-based, inferential perspective used;

  * 4.

a computational framework that leverages the inferential perspective and is
used for computing the result of forgetting operators is presented. It is
based on the use of Ackermann’s Lemma and tautology preserving formula
transformations. This framework is introduced for the propositional case of
forgetting and then later extended to the first-order case;

  * 5.

it is also shown that computing the propositional or first-order (or fixpoint)
equivalent of the dual weak forgetting operator is typically more efficient
then computing the standard forgetting operator, or with computing both the
weakest and strongest necessary conditions. In the light of complexity results
on standard forgetting (see, e.g., [23]), even from that one standpoint alone,
it is beneficial to consider the dual weak forgetting operator as a separate
operator when it is feasible to use representationally.

The rest of the paper is structured as follows. Section 2 presents
preliminaries related to propositional logic and standard forgetting. Section
3 discusses forgetting operators in general and provides their second-order
characterization. In Section 4, some examples are presented illustrating the
approach, where the weak forgetting operator is shown to be very useful
representationally. Section 5 considers the strong relationship between the
dual forgetting operators and strongest necessary and weakest sufficient
conditions. Section 6 shows how the formalism using dual forgetting operators
can be extended to the first-order case, whereas the approach to standard
forgetting and its use has been predominantly propositional in nature. In
Section 7, we discuss relevant, related work. Finally, Section 8 concludes the
paper with a summary and some final remarks.

##  2 Preliminaries

###  2.1 Classical Propositional Logic

For the sake of simplicity, we initially present ideas starting with classical
propositional logic, $\mathcal{L}_{0}$, with truth constants $\mathbb{T}$
(true) and $\mathbb{F}$ (false), an enumerable set of propositional variables
$\mathcal{V}_{0}$, and standard connectives
$\neg,\land,\lor,\rightarrow,\equiv$. We shall also use second-order
quantifiers $\exists p,\forall p$, where $p\in\mathcal{V}_{0}$. The meaning of
quantifiers in the propositional context is:

$\displaystyle\exists
p\big{(}A(p)\big{)}\stackrel{{\scriptstyle\mathrm{def}}}{{\equiv}}A(p=\mathbb{F})\lor
A(p=\mathbb{T});$ (3) $\displaystyle\forall
p\big{(}A(p)\big{)}\stackrel{{\scriptstyle\mathrm{def}}}{{\equiv}}A(p=\mathbb{F})\land
A(p=\mathbb{T}),$ (4)

where $A(p=\mathit{expr})$ denotes a formula obtained from $A$ by substituting
all occurrences of $p$ in $A$ by expression $\mathit{expr}$.

By a theory we mean a finite set of formulas. A theory is identified with a
conjunction of formulas it contains. We often write $\bar{p}$ to denote a
tuple of propositional variables, and $Th(\bar{p})$ to indicate that theory
$Th$ is formed over a vocabulary consisting of variables in $\bar{p}$.
Similarly, we often write $A(\bar{p})$ to indicate that formula $A$ is formed
over a vocabulary consisting of $\bar{p}$.

We say that a formula $A$ is stronger (wrt $\rightarrow$) than a formula $B$,
if $A\rightarrow B$ is a tautology ($\models A\rightarrow B$). In such a case,
we also say that $B$ is weaker (wrt $\rightarrow$) than $A$, $A$ is a
sufficient condition for $B$, and $B$ is a necessary condition for $A$.

A formula $A(p)$ is positive wrt $p\in\mathcal{V}_{0}$, if all occurrences of
$p$ in $A$ are in the scope of an even number of negations.666As usual, we
consider $B\rightarrow C$ to stand for $\neg B\lor C$, and $B\equiv C$ to
stand for $(\neg B\lor C)\land(B\lor\neg C)$. $A(p)$ is negative wrt
$p\in\mathcal{V}_{0}$, if all occurrences of $p$ in $A$ are in the scope of an
odd number of negations. By a literal, we mean a propositional variable or its
negation.

###  2.2 Standard Forgetting

Standard forgetting has been introduced in [26] using a model-theoretic
framework. The intuition behind this operator is to forget a part of the
vocabulary of a theory and remember as much as possible using the remaining
vocabulary, where logical consequences are concerned. Theorem 8 and
Proposition 10 in [26] provide, among others, the following important
properties of forgetting, where $\mathit{forget}(Th(\bar{p},\bar{q}),\bar{p})$
denotes forgetting about $\bar{p}$ in $Th(\bar{p},\bar{q})$.

######  Theorem 2.1 (Lin, Reiter).

Let $\bar{p}$ and $\bar{q}$ be disjoint tuples of propositional variables, $A$
be a formula not containing occurrences of variables from $\bar{p}$ and
$Th(\bar{p},\bar{q})$ be a theory. Then:

$\displaystyle\mbox{--
}\mathit{forget}(Th(\bar{p},\bar{q}),\bar{p})\equiv\exists\bar{p}\big{(}Th(\bar{p},\bar{q})\big{)};$
(5) $\displaystyle\mbox{-- }Th(\bar{p},\bar{q})\models A\mbox{ iff
}\mathit{forget}(Th(\bar{p},\bar{q}),\bar{p})\models A.$ (6)

$\Box$

Notice that (5) can serve as an alternative definition of standard forgetting.
We therefore omit discussion and use of the model-theoretic definition used in
[26]. One can also observe that due to the deduction theorem for classical
propositional logic, (6) can be expressed as:

$\displaystyle\models Th(\bar{p},\bar{q})\rightarrow A\mbox{ iff
}\models\mathit{forget}(Th(\bar{p},\bar{q}),\bar{p})\rightarrow A.$ (7)

###  2.3 An Ackermann-Like Approach to Second-Order Quantifier Elimination

Theorem 2.1(5) indicates that computing forgetting using the Lin&Reiter-like
forgetting operator is equivalent to eliminating second-order quantifiers
$\exists\bar{p}(\ldots)$. While definitions (3)–(4) allow one to eliminate
second-order quantifiers, they lead to an exponential growth of the resulting
formula wrt the number of quantifiers. Therefore, as a computationally more
appropriate tool, we will use the following lemma of Ackermann, already proved
in [2] (see also [11, 19]). This usage typically results in much shorter
formulas as a result of quantifier eliminations in many cases.

######  Lemma 2.2 (Propositional Ackermann Lemma).

Let $A$ be a propositional formula without occurrences of propositional
variable $p$, and $B(p)$ be a propositional formula on a vocabulary containing
$p$:777For the sake of clarity we assume that $B$ contains $p$, but the lemma
is trivially true also when this is not the case.

$\displaystyle\mbox{-- if $B(p)$ is positive wrt\ $p$ then:\; }\exists
p\big{(}(p\rightarrow A)\land B(p)\big{)}\ \equiv\ B(p=A);$ (8)
$\displaystyle\mbox{-- if $B(p)$ is negative wrt\ $p$ then: }\exists
p\big{(}(A\rightarrow p)\land B(p)\big{)}\ \equiv\ B(p=A).$ (9)

$\Box$

The lemma remains true when $p$ is replaced by a second-order variable, say
$P$, representing propositional formulas. For example, (8) can be formulated
as:

$\displaystyle\mbox{-- if $B(P)$ is positive wrt\ $P$ then:\; }\exists
P\big{(}(P\rightarrow A)\land B(P)\big{)}\ \equiv\ B(P=A).$

Lemma (2.2) serves as a blueprint for specifying an algorithm to eliminate
2nd-order quantifiers in many cases. It shows that if one can syntactically
transform a formula $F(\bar{p})$, where $p\in\bar{p}$, into an equivalent
formula with the syntactic structure on the lhs of equivalences (8) or (9),
respectively, then one can eliminate $\exists p$ by substitution of $A$ for
$p$ in $B$, resulting in the equivalent $B(p=A)$. This syntactic technique can
be iterated for all 2nd-order quantifiers in $F(\bar{p})$, resulting in a
logically equivalent propositional formula.

To transform a formula into a form required in (8) or (9), one can use the Dls
algorithm of [11]. For propositional formulas, one of the forms in the
lefthand sides of equivalences (8) or (9) can always be obtained, thus
guaranteeing removal of all 2nd-order quantifiers in an arbitrary
propositional theory.

Figure 1 illustrates the idea behind Ackermann-like lemmas, where the terms
“grows” and “shrinks”, illustrated by dash arrows within ovals, refer to the
standard ordering on truth values, $\mathbb{F}<\mathbb{T}$, compatible with
the semantics of implication, which can be given by:888More formally, we deal
here with the construction of a partial order among formulas for the
Lindenbaum and Tarski algebra [21]. The Lindenbaum–Tarski algebra of a theory
$T$ consists of the equivalence classes of formulas of the theory, where two
formulas are equivalent when the theory $T$ proves that each implies the
other. The partial order in question is then defined as:
$||A||\leq_{T}||B||\mbox{ iff }T\vdash A\rightarrow B,$ where $||C||$ denotes
an equivalence class of a formula $C$.

$(\mbox{the truth value of }p\rightarrow
q)\stackrel{{\scriptstyle\mathrm{def}}}{{=}}(\mbox{`the truth value of
$p$'}\leq\mbox{`the truth value of $q$'}).$

Given the constraint $p\rightarrow A$ in (8) (or, respectively, $A\rightarrow
p$ in (9)), the greatest value of $B(p)$ is obtained when $p$ takes its
greatest (respectively, smallest) value, i.e., the value given by $A$. Of
course, in such cases, the existential quantifier $\exists p(\ldots)$ obtains
the greatest value of $B(p)$, achieved for $p=A$. In this case, each of the
constraints $p\rightarrow A$ (in (8)) as well as $A\rightarrow p$ (in (9))
evaluate to $\mathbb{T}$, and so disappear from the result.

Figure 1: An illustration of intuitions behind Ackermann-like lemmas.

##  3 The Entailment-Based Inferential Perspective on Forgetting

###  3.1 Some Intuitions

Let $Th(\bar{p},\bar{q})$ be a propositional theory over a vocabulary
consisting of $\bar{p},\bar{q}$.999When we refer to tuples of variables as
arguments, like in $Th(\bar{p},\bar{q})$, we always assume that $\bar{p}$ and
$\bar{q}$ are disjoint. When forgetting $\bar{p}$ in the theory
$Th(\bar{p},\bar{q})$, one can delineate two alternative views, one existing
and one new, with both resulting in a theory expressed in the vocabulary
containing $\bar{q}$ only:

  * 1.

strong (standard) forgetting
$F^{NC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}$: a theory that preserves the
entailment of necessary conditions over $\bar{q}$;

  * 2.

weak forgetting $F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}$: a theory
that preserves the entailment of sufficient conditions over $\bar{q}$.

The rationale behind the operator
$F^{NC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}$ is that one wants to
remember a theory on vocabulary $\bar{q}$, whose consequences are also
consequences of the original theory. That is, for any formula $A$ on a
vocabulary disjoint with $\bar{p}$,

$\models Th(\bar{p},\bar{q})\rightarrow A\mbox{ iff }\models
F^{NC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\rightarrow A.$ (10)

In this case, a formula $A$ is a consequence of the result of forgetting,
$F^{NC}\big{(}\big{)}$, iff it is a consequence of the original theory
$Th(\bar{p},\bar{q})$. Notice the similarity of (7) and (10) indicating that
$\mathit{forget}()$ and $F^{NC}\big{(}\big{)}$ act in the same manner.
However, while in the approach of [26], the property (7) is a derived theorem,
in our approach it is a fundamental starting point.

The rationale behind the weak forgetting operator
$F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}$ is that one wants to
remember a theory on vocabulary $\bar{q}$ such that a formula implies
$F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}$ iff it implies the original
theory. That is, for any formula $A$ on a vocabulary disjoint with $\bar{p}$,

$\models A\rightarrow Th(\bar{p},\bar{q})\mbox{ iff }\models A\rightarrow
F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}.$ (11)

That is, a formula $A$ implies the result of weak forgetting,
$F^{SC}\big{(}\big{)}$, iff it implies the original theory
$Th(\bar{p},\bar{q})$.

###  3.2 The Operator $F^{NC}\big{(}\big{)}$

The requirement (10) that $F^{NC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}$
preserves the entailment of necessary conditions over a vocabulary disjoint
with $\bar{p}$ can be expressed as:

$\forall P\Big{(}\forall\bar{p}\big{(}Th(\bar{p},\bar{q})\rightarrow
P\big{)}\equiv\big{(}F^{NC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\rightarrow
P\big{)}\Big{)},$ (12)

where $P$ is a second-order variable representing an arbitrary formula over a
vocabulary disjoint with $\bar{p}$.

Using (12) as a basis, let’s derive an important Theorem 3.1, characterizing
the operator, $F^{NC}\big{(}\big{)}$. By a standard propositional tautology,
we represent equivalence $\equiv$ in (12) as the conjunction of left-to-right
($\rightarrow$) and right-to-left ($\leftarrow$) implications.

####  3.2.1 The Analysis of the Left-to-Right Direction

Let us start with the analysis of the left-to-right direction ($\rightarrow$)
of (12). Since variables $\bar{p}$ occur only in $Th(\bar{p},\bar{q})$, the
implication is equivalent to:

$\forall
P\Big{(}\big{(}\exists\bar{p}\big{(}Th(\bar{p},\bar{q})\big{)}\rightarrow
P\big{)}\rightarrow\big{(}F^{NC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\rightarrow
P\big{)}\Big{)},$ (13)

In order to apply Lemma 2.2, we have to transform (13) into an equivalent
form:

$\neg\exists
P\Big{(}\big{(}\exists\bar{p}\big{(}Th(\bar{p},\bar{q})\big{)}\rightarrow
P\big{)}\land F^{NC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\land\neg
P\Big{)}.$ (14)

We eliminate the second-order quantifier $\exists P$ from (14) using Lemma
2.2(9). As a result we obtain the following formula equivalent to (14):

$\begin{array}[]{l}\neg\Big{(}F^{NC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\land\neg\exists\bar{p}\big{(}Th(\bar{p},\bar{q})\big{)}\Big{)},\end{array}$
(15)

which in turn is equivalent to:

$\begin{array}[]{l}F^{NC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\rightarrow\exists\bar{p}\big{(}Th(\bar{p},\bar{q})\big{)}.\end{array}$
(16)

####  3.2.2 The Analysis of the Right-to-Left Direction

For the right-to-left direction ($\leftarrow$) of (12) we proceed as follows.
Since variables $\bar{p}$ occur only in $Th(\bar{p},\bar{q})$, the implication
($\leftarrow$) is equivalent to:

$\forall
P\Big{(}\big{(}F^{NC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\rightarrow
P\big{)}\rightarrow\big{(}\exists\bar{p}\big{(}Th(\bar{p},\bar{q})\big{)}\rightarrow
P\big{)}\Big{)},$ (17)

which is equivalent to:

$\neg\exists
P\Big{(}\big{(}F^{NC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\rightarrow
P\big{)}\land\exists\bar{p}\big{(}Th(\bar{p},\bar{q})\big{)}\land\neg
P\Big{)}.$ (18)

As before, we eliminate the second-order quantifier $\exists P$ from (18)
using Lemma 2.2(9). As a result, we obtain the following formula equivalent to
(14):

$\neg\Big{(}\exists\bar{p}\big{(}Th(\bar{p},\bar{q})\big{)}\land\neg
F^{NC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\Big{)},$ (19)

which in turn is equivalent to:

$\begin{array}[]{l}\exists\bar{p}\big{(}Th(\bar{p},\bar{q})\big{)}\rightarrow
F^{NC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}.\end{array}$ (20)

####  3.2.3 A Characterization of $F^{NC}\big{(}\big{)}$

Using (16), (20) and Theorem 2.1 (5), we have the following characterization
of $F^{NC}\big{(}\big{)}$.

######  Theorem 3.1.

For arbitrary tuples of propositional variables $\bar{p},\bar{q}$ and
$Th(\bar{p},\bar{q})$,

  1. 1.

$F^{NC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\equiv\exists\bar{p}\big{(}Th(\bar{p},\bar{q})\big{)}.$

  2. 2.

$F^{NC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\equiv\mathit{forget}(Th(\bar{p},\bar{q});\bar{p})$.

  3. 3.

$F^{NC}\big{(}Th(\bar{p},\bar{q}),\bar{p}\big{)}$ is the strongest (wrt
$\rightarrow$) formula over vocabulary $\bar{q}$, satisfying (12). $\Box$

###  3.3 The Operator $F^{SC}\big{(}\big{)}$

By analogy to $F^{NC}\big{(}\big{)}$, the requirement (11) that
$F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}$ preserves entailment by
sufficient conditions can be expressed as:

$\forall P\Big{(}\big{(}P\rightarrow
F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\big{)}\equiv\forall\bar{p}\big{(}P\rightarrow
Th(\bar{p},\bar{q})\big{)}\Big{)},$ (21)

where $P$ is again a second-order variable representing an arbitrary formula
over a vocabulary disjoint with $\bar{p}$. As in Section 3.2, we represent
equivalence $\equiv$ in (21) as the conjunction of two implications
($\rightarrow$) and ($\leftarrow$).

####  3.3.1 The Analysis of the Left-to-Right Direction

Let us first consider implication ($\rightarrow$). Since $P$ is $\bar{p}$
free, the implication is equivalent to:

$\forall P\Big{(}\big{(}P\rightarrow
F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\big{)}\rightarrow\big{(}P\rightarrow\forall\bar{p}\big{(}Th(\bar{p},\bar{q})\big{)}\big{)}\Big{)}.$
(22)

To apply Lemma 2.2, we transform (22) to an equivalent form:

$\neg\exists P\Big{(}\big{(}P\rightarrow
F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\big{)}\land
P\land\neg\forall\bar{p}\big{(}Th(\bar{p},\bar{q})\big{)}\Big{)}.$ (23)

We eliminate the second-order quantifier $\exists P$ from (23), using Lemma
2.2(8). As a result, we obtain the following formula equivalent to (23):

$\begin{array}[]{l}\neg\Big{(}F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\big{)}\land\neg\forall\bar{p}\big{(}Th(\bar{p},\bar{q})\big{)}\Big{)},\end{array}$
(24)

which in turn is equivalent to:

$\begin{array}[]{l}F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\big{)}\rightarrow\forall\bar{p}\big{(}Th(\bar{p},\bar{q})\big{)}.\end{array}$
(25)

####  3.3.2 The Analysis of the Right-to-Left Direction

The implication ($\leftarrow$) of (21) is equivalent to:

$\forall
P\Big{(}\big{(}P\rightarrow\forall\bar{p}\big{(}Th(\bar{p},\bar{q})\big{)}\big{)}\rightarrow\big{(}P\rightarrow
F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\big{)}\Big{)}.$ (26)

To apply Lemma 2.2, we transform (26) to an equivalent form:

$\neg\exists
P\Big{(}\big{(}P\rightarrow\forall\bar{p}\big{(}Th(\bar{p},\bar{q})\big{)}\big{)}\land
P\land\neg F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\Big{)}.$ (27)

We eliminate the second-order quantifier $\exists P$ from (27), using Lemma
2.2(8). As a result, we obtain the following formula equivalent to (27):

$\neg\Big{(}\forall\bar{p}\big{(}Th(\bar{p},\bar{q})\big{)}\land\neg
F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\Big{)}.$ (28)

which in turn is equivalent to:

$\begin{array}[]{l}\forall\bar{p}\big{(}Th(\bar{p},\bar{q})\big{)}\rightarrow
F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\big{)}.\end{array}$ (29)

####  3.3.3 A Characterization of $F^{SC}\big{(}\big{)}$

Combining (25) and (29), we have the following characterization of
$F^{SC}\big{(}\big{)}$.

######  Theorem 3.2.

For arbitrary tuples of propositional variables $\bar{p},\bar{q}$ and
$Th(\bar{p},\bar{q})$,

  1. 1.

$F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\equiv\forall\bar{p}\,\big{(}Th(\bar{p},\bar{q})\big{)}.$

  2. 2.

$F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}$ is the weakest (wrt
$\rightarrow$) formula over vocabulary $\bar{q}$, satisfying (21). $\Box$

###  3.4 Combining $F^{NC}\big{(}\big{)}$ and $F^{SC}\big{(}\big{)}$ in a dual
or complementary perspective

The net result of the analysis provided is that standard or strong forgetting,
and weak forgetting are complementary in an intuitive and formally concise
manner.

Weak forgetting, $F^{SC}\big{(}\big{)}$, allows one to remember more than
using solely standard (strong) forgetting, $F^{NC}\big{(}\big{)}$, relative to
a specific theory. This can be shown to be very useful in applications of
forgetting operators as exhibited in Section 4.

In the original example (1), the weak forgetting operator
$F^{SC}\big{(}\big{)}$ can be applied naturally,

$F^{SC}\big{(}(lt\lor lp);lt\big{)}\equiv\forall\,lt\,(lt\lor lp)\equiv lp$
(30)

As suggested in Section 1, $lt$ is forgotten, while retaining additional
information $lp$ about the physical system.

It is interesting to observe that $F^{NC}\big{(}\big{)}$ and
$F^{SC}\big{(}\big{)}$ partition the theory $Th(\bar{p},\bar{q})$ into three
nicely related classes of formulas (see Figure 2):

  * 1.

the innermost oval, $F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}$:
formulas in vocabulary $\bar{q}$ that imply the original theory (sufficient
conditions of the theory);

  * 2.

the central oval: the original theory $Th(\bar{p},\bar{q})$;

  * 3.

the outermost oval, $F^{NC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}$:
formulas in vocabulary $\bar{q}$ implied by the original theory (necessary
conditions of the theory).

Figure 2: The relationships between forgetting operators and the original
theory in terms of entailment: the ovals inclusion indicates that the formula
in an inner oval entails the formula in an outer one.

From another perspective,

  * 1.

$F^{NC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}$ is “the best” upper
approximation of $Th(\bar{p},\bar{q})$ using the restricted vocabulary (as
shown in point 3 of Theorem 3.1);

  * 2.

$F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}$ is “the best” lower
approximation of $Th(\bar{p},\bar{q})$ using the restricted vocabulary (as
shown in point 2 of Theorem 3.2).

###  3.5 The Computational Perspective for Weak Forgetting

The computational overhead involved in computing weak forgetting
$F^{SC}\big{(}\big{)}$ is, in the worst case, the same as for computing
standard forgetting $F^{NC}\big{(}\big{)}$, which is exponential in the size
of the input formula, yet there are some pragmatic distinctions.
Transformations of formulas made for $F^{NC}\big{(}\big{)}$ can many times be
reused in computing $F^{SC}\big{(}\big{)}$. Moreover, frequently there may be
a more substantial complexity gain. Notice that in some applications, theories
are typically presented as sets of formulas,
$Th(\bar{p},\bar{q})=\\{A_{1}(\bar{p},\bar{q}),\ldots,A_{k}(\bar{p},\bar{q})\\}$,
interpreted as the conjunction $Th(\bar{p},\bar{q})\equiv
A_{1}(\bar{p},\bar{q})\land\ldots\land A_{k}(\bar{p},\bar{q}).$ By Theorem
(7),

$\begin{array}[]{ll}F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\equiv\forall\bar{p}\big{(}Th(\bar{p},\bar{q})\big{)}\equiv&\forall\bar{p}\big{(}A_{1}(\bar{p},\bar{q})\land\ldots\land
A_{k}(\bar{p},\bar{q})\big{)}\equiv\\\
&\forall\bar{p}\big{(}A_{1}(\bar{p},\bar{q})\big{)}\land\ldots\land\forall\bar{p}\big{(}A_{k}(\bar{p},\bar{q})\big{)}.\end{array}$

This partitioning allows one to eliminate second-order quantifiers
$\forall{\bar{p}}$ in each conjunct separately. Though this has to be repeated
$k$ times, the formulas involved are smaller, which in typical cases results
in a significant complexity reduction.

Notice also that frequently in applications, the formulas
$A_{1}(\bar{p},\bar{q}),\ldots$, $A_{k}(\bar{p},\bar{q})$ are syntactically
structured in the form of rules/implications (or sequents) of the form:

$\big{(}\ell_{1}\land\ldots\land\ell_{r}\big{)}\rightarrow\big{(}\ell_{r+1}\lor\ldots\lor\ell_{s}\big{)},$
(31)

where $\ell_{i}$ ($i=1,\ldots,s$) are literals. Of course, (31) is equivalent
to
$\neg\ell_{1}\lor\ldots\lor\neg\ell_{r}\lor\ell_{r+1}\lor\ldots\lor\ell_{s}.$
Eliminating second-order quantifiers $\bar{p}$ from:

$\forall\bar{p}\big{(}\neg\ell_{1}\lor\ldots\lor\neg\ell_{r}\lor\ell_{r+1}\lor\ldots\lor\ell_{s}\big{)}$
(32)

is then straightforward, as shown in Algorithm 1.

Data: Formula $A\equiv$ (32)

Result: Formula $B$ equivalent to $A$, without second-order quantifiers.

begin

$B\leftarrow$ the formula obtained from $A$ after removing double negations;

if  _there is a literal and its negation in the resulting clause_ then

$B\leftarrow\mathbb{T}$

else

$B\leftarrow$ the formula obtained from $B$ after removing literals involving
propositional variables from $\bar{p}$, where the empty disjunction that may
be obtained is $\mathbb{F}$

end if

Remove from $B$ quantifiers binding propositional variables in $\bar{p}$

end

Algorithm 1 Eliminating second-order quantifiers from formulas of the form
(32).

The following example illustrates this method.

######  Example 3.3.

Consider the following formula:

$\forall q\forall r\big{(}\neg\neg q\lor\neg r\lor\neg s\lor t\big{)}.$ (33)

After removing double negation in front of $q$, then removing the literals
involving quantified variables (i.e., $q$ and $\neg r$), and finally removing
the quantifiers, the algorithm outputs $(\neg s\lor t)$ as a formula
equivalent to (33). $\Box$

##  4 Some Examples

The first example shows that standard forgetting can be too strong in
scenarios, where formulas (rules) depend on some uncontrolled parameters. That
is, propositions whose truth values depend on the parameter’s values, occur
only in the rule’s premises. In such cases, when a parameter’s value becomes
unknown, e.g., due to a failure of a measuring device, one would like to
forget the corresponding proposition as this becomes meaningless. In standard
forgetting, all rules involving such propositions disappear, reducing to
$\mathbb{T}$.

######  Example 4.1.

Consider a toy expert system for maintaining a proper balance between
temperature and pressure in a production process. While the pressure can be
controlled, we assume that outside temperature is not controllable. Let:

  * 1.

$mt,ht$ stand for “medium” and “high temperature”;

  * 2.

$lp,mp$ stand for “maintain low” and “mantain medium pressure”.

The considered theory, $Th(mt,ht,lp,mp)$, consists of the following formulas:

$\displaystyle mt\rightarrow lp\lor mp;$ (34) $\displaystyle ht\rightarrow
lp.$ (35)

Assume the temperature sensor is broken and one wants to forget related
propositions $mt,ht$. Using Theorems 3.1(1) and Theorem 3.2(1), simple
transformations of formulas, and Lemma 2.2, we obtain that:

  * 1.

$F^{NC}\big{(}Th(mt,ht,lp,mp);mt,ht\big{)}$ is equivalent to $\mathbb{T}$.

  * 2.

$F^{SC}\big{(}Th(mt,ht,lp,mp);mt,ht\big{)}$ is equivalent to $(lp\lor mp)\land
lp$, being equivalent to $lp$.

Notice that $F^{SC}\big{(}\big{)}$ is much more informative: when the
temperature is unknown, for safety reasons it is better to maintain low
pressure ($lp$) as a sufficient condition for satisfying rules (34), (35).
$\Box$

The following example illustrates the use of forgetting when there are
restrictions on accessing sensitive, personal data directly from a specific
person or belief base. One gets around this by leveraging implicit information
about that person through an inferential process that involves the use of
forgetting.

######  Example 4.2.

Assume Eve works in human resources in a company where Joe is employed. Eve
faces some cultural barriers, or legislative restrictions, in asking Joe about
his potential addiction to alcohol or drugs. In order to find the answer, she
may use some extra knowledge/beliefs in addition to some neutral questions or
observations in probing for an answer. To illustrate the approach consider a
belief, expressed by the following simple formula, where $fdd$ stands for
“frequently denies driving”, $ld$ stands for “likes driving”, and $pa$ stands
for “potentially addicted”:

$fdd\rightarrow(\neg ld\lor pa).$ (36)

When using (36) to detect Joe’s potential addiction to alcohol or drugs, Eve
may wonder when this formula implies $pa$, without referring to $pa$ itself.
That is, she might be interested in the theory:

$Th(pa,ld,fdd)\stackrel{{\scriptstyle\mathrm{def}}}{{\equiv}}\big{(}\underbrace{(fdd\rightarrow(\neg
ld\lor pa))}_{\mbox{\eqref{eq:addict}}}\rightarrow pa\big{)},$

but forgetting about $pa$. In this case, weak forgetting can be used:

$F^{SC}\big{(}Th(pa,ld,fdd);pa\big{)}.$ (37)

According to Theorem 3.2(1), (37) is equivalent to:

$\forall pa\big{(}(fdd\rightarrow(\neg ld\lor pa))\rightarrow pa\big{)},$ (38)

which is equivalent to:

$\neg\exists pa\big{(}(fdd\rightarrow(\neg ld\lor pa))\land\neg pa\big{)}.$
(39)

Formula (39) can easily be transformed into a form required for application of
Lemma 2.2:

$\neg\exists pa\big{(}(\underbrace{pa\rightarrow\mathbb{F}}_{\neg
pa})\land(fdd\rightarrow(\neg ld\lor pa))\big{)}.$

Now Lemma 2.2(8) results in the following equivalent formula:

$\neg\big{(}fdd\rightarrow(\neg
ld\lor\mathbb{F})\big{)}\equiv\neg\big{(}fdd\rightarrow\neg ld\big{)}\equiv
fdd\land ld.$ (40)

To derive the conclusion that Joe is potentially addicted ($pa$), Eve might
try to find out independently, whether Joe frequently denies driving while at
the same time likes driving. If both these assertions are true, then $pa$ is
true too.

Observe that $F^{NC}\big{(}Th(pa,ld,fdd);pa\big{)}$ is equivalent to:

$\exists pa\big{(}(fdd\rightarrow(\neg ld\lor pa))\rightarrow pa\big{)},$

which is equivalent to $\mathbb{T}$ (with witness
$pa\stackrel{{\scriptstyle\mathrm{def}}}{{\equiv}}\mathbb{T}$). So, it could
not be used in this particular context. $\Box$

The last example in this section is inspired by applying forgetting to the
problem of restoring consistency of belief bases merged from different sources
[24].

######  Example 4.3.

Assume that Jack (the first source) considers building an outdoor recreational
complex consisting of tennis courts ($tc$) and a swimming pool ($sp$). He
allocates a budget for the investments. Let ‘$bdg$’ expresses that the overall
investment fits in the budget, ‘$loan$’ stand for getting a loan and ‘$inv$’
denote involvement of an additional investor. Jack’s requirements are then
expressed as:

$tc\land sp\land(bdg\lor loan\lor inv).$ (41)

He hires an external consultant (the second source) who believes that in
addition to outdoor sport facilities, an indoor squash court ($isq$) and a gym
center ($gc$) are necessary to attract enough customers. This can be expressed
by $\\!\\!\\!\\!\\!\\!\\!\\!\\!\underbrace{(tc\lor sp)}_{\mbox{outdoor
facilities}}\\!\\!\\!\\!\\!\\!\\!\\!\\!\rightarrow(isq\land gc)$. The
consultant is well aware of specific costs for the different centers and
courts. Consequently, the consultant believes that building an additional
indoor squash court will not require a loan ($isq\rightarrow\neg loan$), while
for a gym center a loan will be needed ($gc\rightarrow loan$). Summing up, the
external consultant’s beliefs can be expressed as:

$\big{(}(tc\lor sp)\rightarrow(isq\land
gc)\big{)}\land\big{(}isq\rightarrow\neg loan\big{)}\land\big{(}gc\rightarrow
loan\big{)}.$ (42)

Jack’s beliefs, expressed by (41), merged with the consultant’s beliefs, which
are expressed by (42), are jointly inconsistent on ‘$loan$’. The investor
decides to forget about ‘$loan$’. According to consistency restoring
strategies considered in [24], in order to derive meaningful conclusions, Jack
can forget about ‘$loan$’ in selected parts of the merged belief bases. Assume
that he considers forgetting ‘$loan$’ in (41) or (42):

– $\displaystyle
F^{NC}\big{(}\\{\eqref{eq:tennisswimming}\\};loan\big{)}\equiv tc\land sp,$
(43) $\displaystyle\qquad
F^{SC}\big{(}\\{\eqref{eq:tennisswimming}\\};loan\big{)}\equiv tc\land
sp\land(bdg\lor inv);$ (44) – $\displaystyle
F^{NC}\big{(}\\{\eqref{eq:consultant}\\};loan\big{)}\equiv\big{(}(tc\lor
sp)\rightarrow(isq\land gc)\big{)}\land\big{(}isq\rightarrow\neg gc),$ (45)
$\displaystyle\qquad
F^{SC}\big{(}\\{\eqref{eq:consultant}\\};loan\big{)}\equiv\big{(}(tc\lor
sp)\rightarrow(isq\land gc)\big{)}\land\neg isq\land\neg gc.$ (46)

Notice that weak forgetting $F^{SC}\big{(}\big{)}$ adds substantial additional
informative content in comparison to standard forgetting
$F^{NC}\big{(}\big{)}$, by providing sufficient conditions for the respective
formulas:

  * 1.

(44) extends (43) by information that to satisfy the formula (41) after
forgetting about ‘$loan$’, it suffices that additionally $(bdg\lor inv)$
holds;

  * 2.

(46) extends (45) by information that to satisfy the formula (42) after
forgetting about ‘$loan$’, it suffices that additionally $\neg isq$ and $\neg
gc$ hold. $\Box$

Although the examples considered may seem somewhat contrived due to their
brevity, they do target deeper generic applications in which forgetting
operators can play a substantial inferential role. Additionally, the pragmatic
use and importance of the weak forgetting operator is clearly shown as a
useful inferential complement to the standard forgetting operator.

##  5 Relationship with Strongest Necessary and Weakest Sufficient Conditions

Strongest necessary and weakest sufficient conditions have been introduced in
[25]. Let us recall the definitions with minor adjustments.

By a necessary condition of a formula $A(\bar{p},\bar{q})$ on propositional
variables $\bar{q}$ under theory $Th(\bar{p},\bar{q})$ we shall understand any
formula $B(\bar{q})$ containing only symbols in $\bar{q}$ such that$T\models
A(\bar{p},\bar{q})\rightarrow B(\bar{q})$. Such a formula $B(\bar{q})$ is the
strongest necessary condition, denoted by
$\mathit{snc}\big{(}Th(\bar{p},\bar{q});A(\bar{p},\bar{q});\bar{q}\big{)}$ if,
additionally, for any necessary condition $C(\bar{q})$ of $A(\bar{p},\bar{q})$
on $\bar{q}$ under $Th(\bar{p},\bar{q})$, we have that
$T(\bar{p},\bar{q})\models B(\bar{q})\rightarrow C(\bar{q})$.

By a sufficient condition of a formula $A(\bar{p},\bar{q})$ on propositional
variables $\bar{q}$ under theory $Th(\bar{p},\bar{q})$ we shall understand any
formula $B(\bar{q})$ containing only symbols in $\bar{q}$ such that
$Th(\bar{p},\bar{q})\models B(\bar{q})\rightarrow A(\bar{p},\bar{q})$. It is
the weakest sufficient condition, denoted by
$\mathit{wsc}\big{(}Th(\bar{p},\bar{q});A(\bar{p},\bar{q});\bar{q}\big{)}$ if,
additionally, for any sufficient condition $C(\bar{q})$ of
$A(\bar{p},\bar{q})$ on $\bar{q}$ under $Th(\bar{p},\bar{q})$, we have that
$Th(\bar{p},\bar{q})\models C(\bar{q})\rightarrow B(\bar{q})$.

The following second-order characterization of $\mathit{snc}\big{(}\big{)}$
and $\mathit{wsc}\big{(}\big{)}$ has been provided in [13].

######  Lemma 5.1.

For any $A(\bar{p},\bar{q})$, $\bar{q}$ and $T(\bar{p},\bar{q})$:

$\displaystyle\;\mathit{snc}\big{(}Th(\bar{p},\bar{q});A(\bar{p},\bar{q});\bar{q}\big{)}\equiv\exists\bar{p}\big{(}Th(\bar{p},\bar{q})\land
A(\bar{p},\bar{q})\big{)};$ (47)
$\displaystyle\;\mathit{wsc}\big{(}Th(\bar{p},\bar{q});A(\bar{p},\bar{q});\bar{q}\big{)}\equiv\forall\bar{p}\big{(}Th(\bar{p},\bar{q})\rightarrow
A(\bar{p},\bar{q})\big{)}.$ (48)

$\Box$

By use of Theorem 3.1(1), Theorem 3.2(1) and Lemma 5.1, the following
corollary shows that the dual forgetting operators and strongest necessary and
weakest sufficient conditions are mutually definable.

######  Corollary 5.2.

$\displaystyle\;\mathit{snc}\big{(}Th(\bar{p},\bar{q});A(\bar{p},\bar{q});\bar{q}\big{)}\\!\equiv\\!F^{NC}\big{(}Th(\bar{p},\bar{q})\land
A(\bar{p},\bar{q});\bar{p}\big{)};$ (49)
$\displaystyle\;\mathit{wsc}\big{(}Th(\bar{p},\bar{q});A(\bar{p},\bar{q});\bar{q}\big{)}\\!\equiv\\!F^{SC}\big{(}Th(\bar{p},\bar{q})\\!\rightarrow\\!A(\bar{p},\bar{q});\bar{p}\big{)};$
(50)
$\displaystyle\;F^{NC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\equiv\mathit{snc}\big{(}Th(\bar{p},\bar{q});\mathbb{T};\bar{q}\big{)};$
(51)
$\displaystyle\;F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}\equiv\mathit{wsc}\big{(}\neg
Th(\bar{p},\bar{q});\mathbb{F};\bar{q}\big{)}.$ (52)

$\Box$

Even though Corollary 5.2 exists, notice that forgetting operators typically
serve purposes different than those of strongest necessary and weakest
sufficient conditions. That is, the operators $\mathit{snc}\big{(}\big{)}$ and
$\mathit{wsc}\big{(}\big{)}$ focus on queries $A(\bar{p},\bar{q})$ to, or
observations complementing a theory $Th()$, when the underlying language is
reduced. In applying $F^{NC}\big{(}\big{)}$ and $F^{SC}\big{(}\big{)}$, one
looks for the “best” approximations of the theory in a reduced sublanguage.
For example,

  * 1.

the weakest sufficient condition
$\mathit{wsc}\big{(}Th(\bar{p},\bar{q});A(\bar{p},\bar{q});\bar{q}\big{)}$ can
be used to explain the query (observation), $A(\bar{p},\bar{q})$, given the
theory $Th(\bar{p},\bar{q})$, in a sublanguage consisting of $\bar{q}$;

  * 2.

on the other hand, the associated weak forgetting operator
$F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}$, can be used to explain the
theory $Th(\bar{p},\bar{q})$ in the same sublanguage, consisting of $\bar{q}$.

As an added distinction, computing
$F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}$ is usually more efficient
than computing
$\mathit{wsc}\big{(}Th(\bar{p},\bar{q});A(\bar{p},\bar{q});\bar{q}\big{)}$
(see also Sections 3.5 and 6.4).

##  6 A First-Order Extension

Generalization of forgetting operators to the first-order case is an important
topic of research and also essential for many applications [9, 14, 26].
Although limited work has been done with standard forgetting, there are no
general, generic approaches in this respect. In approaching this topic,
classical first- and second-order logics [7, 19] will be used, assuming the
following languages:

  * 1.

classical first-order logic, $\mathcal{L}_{1}$, extending propositional logic
$\mathcal{L}_{0}$ with the set $\mathcal{V}_{1}$ of individual variables
representing domain objects, $\cal R$ of relation symbols, and first-order
quantifiers $\forall,\exists$ binding individual variables;

  * 2.

second-order logic, $\mathcal{L}_{2}$, extending $\mathcal{L}_{1}$ with
relational variables, $\mathcal{V}_{2}$, and second-order quantifiers, also
denoted by $\forall,\exists$, but binding relational variables.

Some additional terminology is also required. The part of a logical formula to
which a quantifier is applied is called the scope of this quantifier. A
quantifier binds its variable within its scope. An occurrence of a variable in
a formula is bound if it occurs in the scope of a quantifier binding the same
variable. Otherwise the occurrence of this variable is free. A formula not
containing free variables is called closed.

###  6.1 First-Order Standard and Weak Forgetting

When shifting from entailment (6) to implication (7), the deduction theorem
for propositional logic was applied. In first-order logic, the deduction
theorem requires that the formulas moved from the left-hand side to the right-
hand side of $\models$, are closed. That is, in the first-order case there
will be the requirement that the theories considered contain only closed
formulas. In practice, this is not really a restriction. Typically, belief
bases are defined using closed formulas. Even if the formulas in question
contain free variables, such as in rule-based theories, they are assumed to be
implicitly universally quantified.

Given the above requirement pertaining to closed theories, considerations
about standard and weak forgetting provided in Section 3, including Theorems
3.1 and 3.2, are preserved. This is formulated in the following theorems,
where for tuples of relation symbols $\bar{r},\bar{s}$, $Th(\bar{r},\bar{s})$
is a closed first-order theory over vocabulary $\bar{r},\bar{s}$ and, rather
than in the propositional version (12), (21), there is the requirement that
for every second-order variable $P$ representing first-order formulas over a
vocabulary disjoint with $\bar{r}$:

  * 1.

$F^{NC}\big{(}Th(\bar{r},\bar{s});\bar{r}\big{)}$ preserves the entailment of
necessary conditions:

$\forall P\Big{(}\forall\bar{r}\big{(}Th(\bar{r},\bar{s})\rightarrow
P\big{)}\equiv\big{(}F^{NC}\big{(}Th(\bar{r},\bar{s});\bar{r}\big{)}\rightarrow
P\big{)}\Big{)};$ (53)

  * 2.

$F^{SC}\big{(}Th(\bar{p},\bar{q});\bar{p}\big{)}$ preserves the entailment by
sufficient conditions:

$\forall P\Big{(}\big{(}P\rightarrow
F^{SC}\big{(}Th(\bar{r},\bar{s});\bar{r}\big{)}\big{)}\equiv\forall\bar{r}\big{(}P\rightarrow
Th(\bar{r},\bar{s})\big{)}\Big{)}.$ (54)

######  Theorem 6.1.

For arbitrary tuples of relation symbols $\bar{r},\bar{s}$ and a closed first-
order theory $Th(\bar{r},\bar{s})$,

  1. 1.

$F^{NC}\big{(}Th(\bar{r},\bar{s});\bar{r}\big{)}\equiv\exists\bar{r}\,\big{(}Th(\bar{r},\bar{s})\big{)}.$

  2. 2.

$F^{NC}\big{(}Th(\bar{r},\bar{s});\bar{r}\big{)}\equiv\mathit{forget}(Th(\bar{r},\bar{s});\bar{r})$.

  3. 3.

$F^{NC}\big{(}Th(\bar{r},\bar{s}),\bar{r}\big{)}$ is the strongest (wrt
$\rightarrow$) formula over vocabulary $\bar{s}$, satisfying (53). $\Box$

Notice that similarly to the the case of Theorem 3.1.2, Theorem 6.1.2 follows
from the first statement in the above theorem together with Theorem 8 of [26].

######  Theorem 6.2.

For arbitrary tuples of relation symbols $\bar{r},\bar{s}$ and a closed first-
order theory $Th(\bar{r},\bar{s})$,

  1. 1.

$F^{SC}\big{(}Th(\bar{r},\bar{s});\bar{r}\big{)}\equiv\forall\bar{r}\big{(}Th(\bar{r},\bar{s})\big{)}.$

  2. 2.

$F^{SC}\big{(}Th(\bar{r},\bar{s});\bar{r}\big{)}$ is the weakest (wrt
$\rightarrow$) formula over vocabulary $\bar{s}$, satisfying (54). $\Box$

###  6.2 First-Order Ackermann Lemma

As in the propositional case, the first-order Ackermann Lemma provides a
powerful technique for eliminating second-order quantifiers from standard and
weak forgetting formulas. The Dls algorithm of [11] uses Lemma 6.3, described
below.

In order to formulate the first-order version of the Ackermann lemma, let us
extend the notation $A(p=\mathit{expr})$ form Section 2. If $A$ is a formula,
$r$ is a $k$-argument relation symbol occurring in $A$,
$\mathit{expr}(x_{1},\ldots,x_{k})$ is an expression including variables among
$x_{1},\ldots,x_{k}$, then:

$A\big{(}r(x_{1},\ldots,x_{k})=\mathit{expr}(x_{1},\ldots,x_{k})\big{)}$

denotes a formula obtained from $A$ by substituting all occurrences of $r$ by
$\mathit{expr}(x_{1},\ldots,x_{k})$ in which variables $x_{1},\ldots,x_{k}$
are in each instance replaced by arguments of the occurrence of $r$ being
substituted. For example, let
$A\\!\stackrel{{\scriptstyle\mathrm{def}}}{{=}}\\!\big{(}s(x_{1},a)\lor
r(a,b)\lor r(b,c)\big{)}$ and
$\mathit{expr}(x_{1},x_{2})\\!\stackrel{{\scriptstyle\mathrm{def}}}{{=}}\\!s(x_{1},x_{2})\land
t(x_{2},d)$. When $r(x_{1},x_{2})=\mathit{expr}(x_{1},x_{2})$, we have:

$`r(a,b)=\mathit{expr}(a,b)\mbox{'\;is\;}s(a,b)\land t(b,d)\mbox{\;\; and
\;\;}`r(b,c)=\mathit{expr}(b,c)\mbox{'\;is\;}s(b,c)\land t(c,d).$

Therefore we have:

$A\big{(}r(x_{1},x_{2})=\underbrace{(s(x_{1},x_{2})\land
t(x_{2},d))}_{\mathit{expr}(x_{1},x_{2})}\big{)}=s(x_{1},a)\lor\underbrace{(s(a,b)\land
t(b,d))}_{r(a,b)=\mathit{expr}(a,b)}\lor\underbrace{(s(b,c)\land
t(c,d))}_{r(b,c)=\mathit{expr}(b,c)}$

We can now formulate the first-order version of the Ackermann lemma.

######  Lemma 6.3 (First-order Ackermann Lemma).

Let $r$ be a $k$-ary relation symbol, $A$ be a first-order formula without
occurrences of $r$, $B$ be a first-order formula and $\bar{x}$ be a $k$-tuple
of distinct variables. Then:

$\displaystyle\mbox{-- if $B$ is positive wrt\ $r$ then:\; }\exists
r\big{(}\forall\bar{x}(r(\bar{x})\rightarrow A(\bar{x}))\land B\big{)}\
\equiv\ B(r(\bar{x})=A(\bar{x}));$ (55) $\displaystyle\mbox{-- if $B$ is
negative wrt\ $r$ then: }\exists r\big{(}\forall\bar{x}(A(\bar{x})\rightarrow
r(\bar{x}))\land B\big{)}\ \equiv\ B(r(\bar{x})=A(\bar{x})).$ (56)

$\Box$

Observe that Figure 1 also illustrates Lemma 6.3, where $A$ grows when $r$
grows (respectively shrinks).101010In Figure 1, $r$ is represented by $p$. In
the first-order case, Figure 1 is even more intuitive since growing and
shrinking pertains to the tuples that satisfy the relation $r$ ($p$ in the
figure), which are maximized (minimized) relative to (55) and (56),
respectively.

To transform a formula into a form required in (55) or (56), one can again use
the Dls algorithm [11]. Unlike the propositional case, in the first-order case
such a transformation is not always doable in general, but it has been shown
to work for large classes of formulas [6, 11, 19].

The following example illustrates the use of Lemma 6.3 in the context of
standard and weak forgetting.

######  Example 6.4.

To illustrate the use of the first-order Ackermann lemma, consider the
following belief base, where $ms(x)$ stands for “person $x$ has mild symptoms
of a disease”, $ss(x)$ – for “person $x$ has severe symptoms of the disease”,
$h(x)$ – for “$x$ should stay home”, $t(x)$ – for “$x$ needs a test for the
disease”, and $ich(x)$ – for “$x$ should immediately consult a health care
provider”:

$Th(ms,h,t,ss,ich)=\Big{\\{}\forall x\Big{(}ms(x)\rightarrow\big{(}h(x)\land
t(x)\big{)}\Big{)},\;\forall x\Big{(}\big{(}ss(x)\lor t(x)\big{)}\rightarrow
ich(x)\big{)}\Big{)}\Big{\\}}.$ (57)

When a test is not available, it is useful to forget about it, so one can
consider standard and weak forgetting operators
$F^{NC}\big{(}Th\big{(}ms,h,t,ss,ich\big{)};t)\big{)}$ and
$F^{SC}\big{(}Th\big{(}ms,h,t,ss,ich\big{)};t)\big{)}$:

  * 1.

$\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\begin{array}[]{ll}F^{NC}\big{(}Th\big{(}ms,h,t,ss,ich\big{)};t)\big{)}\equiv\exists
t\Big{(}&\\!\\!\\!\\!\\!\\!\forall x\Big{(}ms(x)\rightarrow\big{(}h(x)\land
t(x)\big{)}\Big{)}\land\\\ &\\!\\!\\!\\!\\!\\!\forall x\Big{(}\big{(}ss(x)\lor
t(x)\big{)}\rightarrow ich(x)\Big{)}\Big{)}.\end{array}$ (58)

In order to eliminate $\exists t$ from (58) using Lemma 6.3, it suffices to
transform it to the equivalent form:111111Notice that in this case, the form
can be automatically obtained using the Dls algorithm.

$\exists t\Big{(}\forall x\Big{(}ms(x)\rightarrow t(x)\Big{)}\land\forall
x\Big{(}ms(x)\rightarrow h(x)\Big{)}\land\forall x\Big{(}\big{(}ss(x)\lor
t(x)\big{)}\rightarrow ich(x)\Big{)}\Big{)}.$ (59)

An application of Lemma 6.3(56) results in:

$\forall x\Big{(}ms(x)\rightarrow h(x)\Big{)}\land\forall
x\Big{(}\big{(}ss(x)\lor ms(x)\big{)}\rightarrow ich(x)\Big{)}.$ (60)

That is, a person with minor symptoms should stay at home. If, under the
circumstances, it is not possible to test for the disease, then the severe or
mild symptoms should suffice to immediately consult (by phone or a visit) the
health care provider. Intuitively, both causes are correct:

    * (a)

by the second formula of the belief base (57), severe symptoms suffice for a
need to immediately consult a health care provider;

    * (b)

by the first formula of the belief base (57), mild symptoms imply a need for
making a test which, in turn, by the second formula of the belief base,
suffices for a need to immediately consult a health care provider.

  * 2.

$\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\begin{array}[]{ll}F^{SC}\big{(}Th\big{(}ms,h,t,ss,ich\big{)};t)\big{)}\equiv\forall
t\Big{(}&\\!\\!\\!\\!\\!\\!\forall x\Big{(}ms(x)\rightarrow\big{(}h(x)\land
t(x)\big{)}\Big{)}\land\\\ &\\!\\!\\!\\!\\!\\!\forall x\Big{(}\big{(}ss(x)\lor
t(x)\big{)}\rightarrow ich(x)\Big{)}\Big{)}.\end{array}$ (61)

After a transformation similar to (59), and distributing $\forall t$ over
conjunctions, one obtains the following equivalent formula:

$\forall t\forall x\Big{(}ms(x)\rightarrow t(x)\Big{)}\land\forall t\forall
x\Big{(}ms(x)\rightarrow h(x)\Big{)}\land\forall t\forall
x\Big{(}\big{(}ss(x)\lor t(x)\big{)}\rightarrow ich(x)\Big{)}.$ (62)

One can now eliminate each conjunct separately:

    * (a)

$\forall t\forall x\Big{(}ms(x)\rightarrow t(x)\Big{)}\\!\equiv\\!\forall
x\neg\exists t\Big{(}ms(x)\land\neg t(x)\Big{)}\\!\equiv\\!\forall
x\neg\exists t\Big{(}\forall x\big{(}\mathbb{F}\rightarrow t(x)\big{)}\land
ms(x)\land\neg t(x)\Big{)}$.

Notice that subformula $\forall x\big{(}\mathbb{F}\rightarrow t(x)\big{)}$ is
added artificially to make the Ackermann Lemma work. It is actually a
tautology so, in conjunction with the other formulas, it does not affect their
truth value. Now an application of Lemma 6.3(56), results in $\forall
x\neg\Big{(}ms(x)\land\neg\mathbb{F}\Big{)}$, which is equivalent to $\forall
x\Big{(}\neg ms(x)\Big{)}$;

    * (b)

in $\forall t\forall x\Big{(}ms(x)\rightarrow h(x)\Big{)}$ the quantifier
$\forall t$ is redundant, so can simply be removed;

    * (c)

$\forall t\forall x\Big{(}\big{(}ss(x)\lor t(x)\big{)}\rightarrow
ich(x)\Big{)}\equiv\forall x\neg\exists t\Big{(}\big{(}ss(x)\lor
t(x)\big{)}\land\neg ich(x)\Big{)}$. We add an artificial conjunct $\forall
x\Big{(}t(x)\rightarrow\mathbb{T}\Big{)}$ which is a tautology, apply Lemma
6.3(55), and obtain an equivalent formula $\forall
x\neg\Big{(}\big{(}ss(x)\lor\mathbb{T}\big{)}\land\neg ich(x)\Big{)}$. This is
equivalent to $\forall x\Big{(}ich(x)\Big{)}$.

Thus, we obtain the following first-order result, equivalent to (62):

$\forall x\Big{(}\neg ms(x)\Big{)}\land\forall x\Big{(}ms(x)\rightarrow
h(x)\Big{)}\land\forall x\Big{(}ich(x)\Big{)},$ (63)

which is equivalent to $\forall x\Big{(}\neg ms(x)\Big{)}\land\forall
x\Big{(}ich(x)\Big{)}$. Indeed, without access to a test, $t(x)$, one can only
make sure that the first formula of (57) is true by assuring that $\forall
x\Big{(}\neg ms(x)\Big{)}$ is true. The second formula of (57) can only be
guaranteed when $\forall x\Big{(}ich(x)\Big{)}$ is true. Though $\forall
x\Big{(}\neg ms(x)\Big{)}\land\forall x\Big{(}ich(x)\Big{)}$ looks rather
useless, it can actually be used to select persons satisfying $\neg ms(x)\land
ich(x)$, thus also satisfying (57). That is, when one reduces the domain to
objects satisfying $\big{(}\neg ms(x)\land ich(x)\big{)}$, the initial theory
is guaranteed to hold for those individuals. $\Box$

The use of $F^{SC}\big{(}\big{)}$ in Example 6.4 has interesting generic
potential in that it allows one to isolate a subdomain of individuals ensuring
the validity of a restricted part of the original theory in question.

###  6.3 The Fixpoint Lemma

Notice that Lemma 6.3 requires that formula $A$ does not contain occurrences
of the eliminated relation symbol. On the other hand, when it does, one may
still obtain useful results for a large class of formulas. To see this,
consider once again the cases shown in Figure 1, where rather than $A$ we
consider $A(p)$. As is well known,121212See, e.g., [1]. given that $A(p)$ is
positive wrt $p$, there exists a smallest and greatest fixpoint for $A(p)$ wrt
$p$. This observation is all that is required to generalize the first-order
extension. The idea is formulated in the following lemma, proved in [28] (see
also, e.g., [13, 19]), where:

  * 1.

$\mathrm{Lfp}\,p.\big{(}A(p)\big{)}$ is the least wrt implication (that is, in
the terminology used in the paper, the strongest) formula $B$ being a fixpoint
of $A(p)$, i.e., satisfying $\models B\equiv A(B)$;

  * 2.

$\mathrm{Gfp}\,p.\big{(}A(p)\big{)}$ is the greatest wrt implication (that is,
in the terminology used in the paper, the weakest) formula being a fixpoint of
$A(p)$.

Intuitively, when the extension of a formula shrinks, it becomes stronger
because it implies more formulas. Likewise, when the extension of a formula
grows, it becomes weaker because it is implied by more formulas. Therefore,
least wrt to implication means strongest and greatest wrt implication means
weakest.

######  Lemma 6.5 (Fixpoint Lemma).

Let $r$ be a $k$-ary relation symbol, $A(r)$ be a first-order formula with
positive occurrences of $r$ only, $B$ be a first-order formula, and $\bar{x}$
be a $k$-tuple of distinct variables. Then:

$\displaystyle\mbox{-- if $B$ is positive wrt\ $r$ then:\; }\exists
r\big{(}\forall\bar{x}(r(\bar{x})\rightarrow A(r))\land B\big{)}\ \equiv\
B\big{(}r(\bar{x})=\mathrm{Gfp}\,r(\bar{x}).\big{(}A(r)\big{)}\big{)};$ (64)
$\displaystyle\mbox{-- if $B$ is negative wrt\ $r$ then: }\exists
r\big{(}\forall\bar{x}(A(r)\rightarrow r(\bar{x}))\land B\big{)}\ \equiv\
B\big{(}r(\bar{x})=\mathrm{Lfp}\,r(\bar{x}).\big{(}A(r)\big{)}\big{)}.$ (65)

$\Box$

Notice that Figure 1 applies also to the fixpoint case formulated in Lemma
6.5, where $A$ grows when $r$ grows (respectively shrinks).131313As in the
first-order case, in Figure 1 $r$ is represented by $p$. Therefore we look for
the greatest (respectively least) $r$ such that $r\equiv A(r)$, i.e., $r$ is a
(greatest or least) fixpoint of $A(r)$.

The following example illustrates an application of this lemma.

######  Example 6.6.

A communication network is being designed. Due to a specific application area,
the designers have to consider special security requirements. In particular
they consider two networks: an internal and an external one. The internal
network nodes should not be externally reachable unless they are protected by
a specialized expensive security component. A part of the underlying belief
base contains, among others, the following formula, where $con(x,y)$ stands
for “nodes $x$ and $y$ are directly connected”, and $r(x,y)$ stands for “$y$
is reachable from $x$”:141414Notice that formula (66) can be obtained as a
translation of a rule defining $r()$ as a transitive closure of $con()$.

$\forall x\forall y\Big{(}\big{(}con(x,y)\lor\exists z\big{(}con(x,z)\land
r(z,y)\big{)}\big{)}\rightarrow r(x,y)\Big{)},$ (66)

Due to the security requirements, the following integrity constraint has to be
preserved when choosing direct network connections, where $ex(x)$ and $in(x)$
denote that node $x$ belongs to the external or internal network,
respectively, and $sec(x)$ denotes that node $x$ is equipped with the security
component:

$\forall y\Big{(}\exists x\big{(}ex(x)\land
r(x,y)\big{)}\rightarrow\big{(}in(y)\rightarrow sec(y)\big{)}\Big{)}.$ (67)

That is, when $y$ is reachable from a node $x$ of an external network
($\exists x\big{(}ex(x)\land r(x,y)\big{)}$) then whenever $y$ is an internal
node ($in(y)$) then it is to be equipped with the security protecting
component ($sec(y)$). To focus on the design of $con()$, the designers prefer
to abstract from $r()$ for the time being, so forget about $r$.

Let us first compute $F^{NC}\big{(}Th(con,r,ex,in,sec);r\big{)}$, where
$Th(con,r,ex,in,sec)$ denotes the conjunction
$\mbox{\eqref{eq:seceample}}\land\mbox{\eqref{eq:seceamplenconstr}}$:

$\displaystyle F^{NC}\big{(}Th(con,r,ex,\,$ $\displaystyle
in,sec);r\big{)}\equiv$ $\displaystyle\exists r\,\Big{(}\forall x\forall
y\Big{(}\big{(}con(x,y)\lor\exists z\big{(}con(x,z)\land
r(z,y)\big{)}\big{)}\rightarrow r(x,y)\Big{)}\land$ (68)
$\displaystyle\;\;\;\;\;\;\forall y\Big{(}\exists x\big{(}ex(x)\land
r(x,y)\big{)}\rightarrow\big{(}in(y)\rightarrow sec(y)\big{)}\Big{)}.$ (69)

Observe that Lemma 6.3 cannot be applied due to (68). However, Lemma 6.5(65)
can still be used and results in:

$\begin{array}[]{ll}\forall y\Big{(}\exists
x\big{(}ex(x)\land\mathrm{Lfp}\,r(x,y).\big{(}con(x,y)\lor\exists
z\big{(}con(x,z)\,\land&\\!\\!\\!\\!r(z,y)\big{)}\big{)}\big{)}\\\
&\rightarrow\big{(}in(y)\rightarrow sec(y)\big{)}\Big{)}.\end{array}$ (70)

The least fixpoint in (70) actually defines $r()$ as the transitive closure of
$con()$.

Using the well-known Knaster and Tarski theorem, the least fixpoint
$\mathrm{Lfp}\,r(x,y).\big{(}A(r)\big{)}$, where
$A(r)\stackrel{{\scriptstyle\mathrm{def}}}{{\equiv}}con(x,y)\lor\exists
z\big{(}con(x,z)\land r(z,y)\big{)}$, is equivalent to a disjunction
$\displaystyle\bigvee_{i}A^{i}(\mathbb{F})$, where $A^{i}$ stands for applying
$A$ $i$ times. Therefore, the formula (70) can be represented by the
conjunction:

$\begin{array}[]{ll}\forall y\Big{(}&\\\ &\exists x\big{(}ex(x)\land
A^{0}(\mathbb{F})\big{)}\rightarrow\big{(}in(y)\rightarrow
sec(y)\big{)}\land\\\ &\exists x\big{(}ex(x)\land
A^{1}(\mathbb{F})\big{)}\rightarrow\big{(}in(y)\rightarrow
sec(y)\big{)}\land\\\ &\ldots\\\ &\exists x\big{(}ex(x)\land
A^{i}(\mathbb{F})\big{)}\rightarrow\big{(}in(y)\rightarrow
sec(y)\big{)}\land\\\ &\ldots\\\ \;\;\;\;\Big{)}.\end{array}$

To compute $F^{SC}\big{(}Th(con,r,ex,in,sec);r\big{)}$, we consider:

$\displaystyle F^{SC}\big{(}Th(con,r,ex,\,$ $\displaystyle
in,sec);r\big{)}\equiv$ $\displaystyle\forall r\,\Big{(}\forall x\forall
y\Big{(}\big{(}con(x,y)\lor\exists z\big{(}con(x,z)\land
r(z,y)\big{)}\big{)}\rightarrow r(x,y)\Big{)}\land$ (71)
$\displaystyle\;\;\;\;\;\;\forall y\Big{(}\exists x\big{(}ex(x)\land
r(x,y)\big{)}\rightarrow\big{(}in(y)\rightarrow sec(y)\big{)}\Big{)}.$ (72)

The quantifier $\forall r$ can be distributed over the conjunction, so one can
consider:

$\displaystyle\forall r\,\forall x\forall y\Big{(}\big{(}con(x,y)\lor\exists
z\big{(}con(x,z)\land r(z,y)\big{)}\big{)}\rightarrow r(x,y)\Big{)}\land$ (73)
$\displaystyle\forall r\forall y\Big{(}\exists x\big{(}ex(x)\land
r(x,y)\big{)}\rightarrow\big{(}in(y)\rightarrow sec(y)\big{)}\Big{)}.$ (74)

To eliminate $\forall r$ from (73), we transform it to the following
equivalent form:

$\neg\exists x\exists y\exists r\,\Big{(}\big{(}con(x,y)\lor\exists
z\big{(}con(x,z)\land r(z,y)\big{)}\big{)}\land\neg r(x,y)\Big{)},$ (75)

equivalent to:

$\neg\exists x\exists y\exists r\,\Big{(}\underbrace{\forall u\forall
w\big{(}r(u,w)\rightarrow(u\not=x\lor w\not=y))\big{)}}_{\neg
r(x,y)}\land\big{(}con(x,y)\lor\exists z\big{(}con(x,z)\land
r(z,y)\big{)}\big{)}\Big{)}.$ (76)

Applying Ackermann’s Lemma 6.3(55) to (76) one obtains:

$\neg\exists x\exists y\Big{(}\big{(}con(x,y)\lor\exists
z\big{(}con(x,z)\land(z\not=x\lor y\not=y)\big{)}\big{)}\Big{)},$ (77)

equivalent to:

$\forall x\forall y\Big{(}\big{(}con(x,y)\rightarrow\forall
z\big{(}con(x,z)\rightarrow z=x\big{)}\big{)}\Big{)},$ (78)

which in turn is equivalent to:

$\forall x\forall z\Big{(}con(x,z)\rightarrow z=x\Big{)}.$ (79)

To eliminate $\forall r$ from (74), we transform it to the following
equivalent form:

$\neg\exists y\exists r\Big{(}\exists x\big{(}ex(x)\land r(x,y)\big{)}\land
in(y)\land\neg sec(y)\Big{)}.$ (80)

Adding an artificial conjunct $\forall x\forall
y\big{(}r(x,y)\rightarrow\mathbb{T}\big{)}$, equivalent to $\mathbb{T}$ (to
ensure the right syntactic structure), and applying Ackermann’s Lemma 6.3(55)
to (80), we obtain:

$\forall y\Big{(}\exists
x\big{(}ex(x)\big{)}\rightarrow\big{(}in(y)\rightarrow sec(y)\Big{)}.$ (81)

Combining (79) and (81) we obtain that:

$\displaystyle F^{SC}\big{(}Th(con,r,ex,\,$ $\displaystyle
in,sec);r\big{)}\equiv$ $\displaystyle\forall x\forall
z\Big{(}con(x,z)\rightarrow z=x\Big{)}\land$ (82) $\displaystyle\forall
y\Big{(}\exists x\big{(}ex(x)\big{)}\rightarrow\big{(}in(y)\rightarrow
sec(y)\Big{)}.$ (83)

That is, to make sure that $Th(con,r,ex,in,sec)$, when $r()$ is forgotten,
nodes can only be connected to themselves and if there is an external node,
then every internal node is to be equipped with the security component. Though
this guarantees that the security requirements are satisfied, the resulting
theory is rather strong. $\Box$

###  6.4 Computational Aspects

Forgetting is typically applied to finite domain knowledge or belief bases and
rule languages. As indicated by the first points of Theorems 3.1 and 3.2,
Computing queries expressed by $F^{NC}\big{(}\big{)}$ is NP-complete, and
those expressed by $F^{SC}\big{(}\big{)}$ is co-NP-complete. On the other
hand, the data complexity of first-order queries obtained using Lemma 6.3 is
PTime and LogSpace [1]. Data complexity of fixpoint queries, thus also queries
obtained from Lemma 6.5, is PTime [1]. Therefore, the approach based on
Ackermann’s Lemma and its fixpoint extension is computationally friendly.

The following approaches to second-order quantifier elimination that have
previously been formulated and implemented are:

  * 1.

using Lemma 6.3 as a basis for the Dls algorithm [11], which first attempts to
transform an arbitrary formula into a form suitable for applying this lemma,
and then uses this lemma as a basis for eliminating quantifiers;

  * 2.

using Lemma 6.5 as a basis for the Dls* algorithm [12], which extends the Dls
algorithm to work with formulas that are suitable for an application of the
fixpoint lemma.

In fact, all calculations carried out in this paper that involve elimination
of second-order quantifiers reflect selected steps used in the Dls or Dls*
algorithms.

As has been shown in Section 3.5, computing propositional equivalents for the
weak forgetting operator is often more efficient than computing such
equivalents for standard forgetting and for weakest sufficient and strongest
necessary conditions. This reasoning can also be extended to the first-order
case as follows, where we consider eliminating the quantifier $\forall r$ from
the formula:

$\forall r\forall\bar{x}\Big{(}r(\bar{x}_{1})\lor\ldots\lor
r(\bar{x}_{m})\lor\neg r(\bar{x}_{m+1})\lor\ldots\lor\neg r(\bar{x}_{n})\lor
A(\bar{z})\Big{)},$ (84)

where $0\leq m\leq n$, $\bar{x}$ contains at least all variables in
$\bar{x}_{1},\ldots,\bar{x}_{n}$, and formula $A$ does not contain relation
symbol $r$. Formula (84) is equivalent to:

$\forall\bar{x}\neg\exists r\Big{(}\neg r(\bar{x}_{1})\land\ldots\land\neg
r(\bar{x}_{m})\land r(\bar{x}_{m+1})\land\ldots\land r(\bar{x}_{n})\land\neg
A(\bar{z})\Big{)},$ (85)

which can be transformed into the equivalent form (e.g., using the Dls
algorithm):

$\forall\bar{x}\neg\exists
r\Big{(}\forall\bar{y}\big{(}r(\bar{y})\rightarrow(\bar{y}\not=\bar{x}_{1}\land\ldots\land\bar{y}\not=\bar{x}_{m})\big{)}\land
r(\bar{x}_{m+1})\land\ldots\land r(\bar{x}_{n})\land\neg A(\bar{z})\Big{)}.$
(86)

After applying Ackermann’s Lemma (6.3) we obtain the following formula
equivalent to (86), thus also equivalent to (84):

$\forall\bar{x}\neg\Big{(}(\bar{x}_{m+1}\not=\bar{x}_{1}\land\ldots\land\bar{x}_{m+1}\not=\bar{x}_{m})\land\ldots\land(\bar{x}_{n}\not=\bar{x}_{1}\land\ldots\land\bar{x}_{n}\not=\bar{x}_{m})\land\neg
A(\bar{z})\Big{)}.$ (87)

Formula (87) can be simplified to:

$\forall\bar{x}\Big{(}\bar{x}_{m+1}=\bar{x}_{1}\lor\ldots\lor\bar{x}_{m+1}=\bar{x}_{m}\lor\ldots\lor\bar{x}_{n}=\bar{x}_{1}\lor\ldots\lor\bar{x}_{n}=\bar{x}_{m}\lor
A(\bar{z})\Big{)}.$ (88)

That is, the length of the resulting formula (88) is at most quadratic in the
length of the input formula (84). Given variables
$\bar{x}_{1},\ldots,\bar{x}_{m},\bar{x}_{m+1},\ldots,\bar{x}_{n}$, one
typically can still substantially simplify the result. Notice that in similar
cases, the fixpoint lemma is not needed (but may be needed for other shapes of
formulas).

When dealing with a conjunction of formulas of the form (84), the quantifier
$\forall r$ can be distributed over conjunction (as, e.g., in (62)), and each
conjunct can be processed separately. This provides a sharp contrast in
comparison with computing $F^{NC}\big{(}\big{)}$, $\mathit{wsc}\big{(}\big{)}$
and $\mathit{snc}\big{(}\big{)}$, where such a distribution is generally not
possible. This is indicated by their syntactic second-order characterizations
given by point 1 of Theorem 3.1, and formulas (47), (48) of Lemma 5.1,
respectively.

It is worth emphasizing that the problem as to whether a second-order formula
is equivalent to a first-order (or fixpoint) formula, is highly undecidable.
So algorithms like Dls, Dls* as well as any other algorithms attempting to do
the same quantifier elimination, have to fail for some input formulas.
However, pragmatic application has shown that these algorithms work for large
classes of formulas (see Section 7 for more a detailed discussion).

##  7 Related Work

Standard forgetting, $\mathit{forget}$(), has been introduced in the
foundational paper [26], where model theoretical definitions and analysis of
properties of the standard $\mathit{forget}$() operator are provided. Its
second-order characterization as well as its entailment preserving property,
as quoted in Theorem 2.1 above, are consequences of this definition. The paper
[26] opened a research subarea, summarized, e.g., in [10] or more recently, in
[14]. In the approach used in the current paper, one begins with an
entailment-based, inferential perspective, as expressed by (10) and (11). This
is directly beneficial for pragmatic application, since this approach leads
directly to algorithms and implementations of the dual forgetting operators.
In addition to introducing a new weak forgetting operator, standard forgetting
is also characterized in this context.

The paper [10] concentrates on introspective forgetting (“forgetting as
becoming ignorant”). It extends modal epistemic logic with modal operators
allowing one to express what is known before and what remains known after
forgetting. It therefore essentially deals with necessary conditions,
corresponding to standard forgetting.

In [14] two types of forgetting are distinguished: (1) forgetting part of the
signature, corresponding to standard forgetting, and (2) forgetting a formula,
related to contracting in the AGM theory of belief change [3, 18]. In the
current paper, both dual operators, weak and strong forgetting, belong to the
first type of forgetting. The extension of this work to forgetting formulas is
an interesting research direction.

A general framework, covering a range of belief changes involving forgetting,
is proposed in [5]. In particular, a commonsense perspective based on belief
change, involving contraction, ignorance introduction, revision/update,
(deductive) abstraction at the level of rules, marginalization, etc., is
proposed. Another general framework for standard-like forgetting is
investigated in [9], where forgetting is regarded as a belief change operator,
independent of the underlying logic. Forgetting is achieved by reducing a part
of a signature in a theory. In that approach, forgetting is specified by the
set of logical consequences of the input theory over the reduced language.
Though providing very interesting characterizations and contexts of
forgetting, the frameworks of [5] and [9] deal with consequences (necessary
conditions) of the considered theories and do not deal with sufficient
conditions, expressed by the weak forgetting operator in this paper.

Papers which consider relations between forgetting and weakest sufficient and
strongest necessary conditions include [16, 17]. In the first of these papers,
forgetting is applied in the context of strongest necessary and weakest
sufficient conditions in Computation Tree Logic (CTL). Axiomatic
characterization of forgetting and an algorithm for computing forgetting are
provided. In addition, weakest sufficient and strongest necessary conditions
are characterized using forgetting (Theorem 9 in [16]). The characterization
is similar in spirit to the Corollaries (49) and (50) in the current paper. In
[17] the results of [16] are transferred into the context of $\mu$-calculus.
Both in CTL and $\mu$-calculus, typical reasoning problems are intractable.
Forgetting in multiagent modal logics, sharing a similar methodology, has been
addressed in [15]. Unlike in [15, 16, 17], in the current paper, both standard
and weak forgetting are considered. The approach isolates broad classes of
formulas for which one can compute first-order or fixpoint equivalents of both
forgetting operators. This in turn, leads to a tractable reasoning-by-querying
machinery.

In [32] a weak forgetting operator has been introduced which differs from the
weak forgetting operator, $F^{SC}\big{(}\big{)}$, used in this paper, and it
has characteristics much more related to the standard forgetting operator,
$F^{NC}\big{(}\big{)}$. While standard forgetting is not always first-order
expressible, the weak operator of [32] has been developed to make sure that
the result of forgetting can always be expressed in first-order logic. Weak
forgetting in the sense of [32] and standard forgetting differ only in the
cases where the result of standard forgetting is not first-order expressible.
This operator does not coincide with the dual weak forgetting operator
$F^{SC}\big{(}\big{)}$. The terminology used in the current paper, reflects
the fact that $F^{SC}\big{(}\big{)}$ and $F^{NC}\big{(}\big{)}$ are dual
operators that formally show the relationship of $F^{SC}\big{(}\big{)}$ to
weakest sufficient conditions and $F^{NC}\big{(}\big{)}$ to strongest
necessary conditions.

A series of papers [8, 22, 33] (see also references there) has addressed
forgetting in description logics. Though description logics are strongly
related to modal logics [4], the papers [8, 22, 33] are methodologically
closer to the approach used in this paper. In [8], forgetting-based abduction
is investigated using weakest sufficient and strongest necessary conditions.
The idea, inspired by [13], is implemented and experimentally verified using
resolution. As in the approach proposed in the current paper, the papers [22,
33] use the Ackermann [2] and fixpoint [28] Lemmas, adjusted to the
description logic formalism. Though directly dealing with abduction, the
approaches in [8, 22, 33] concentrate on (valuable and important) experimental
research and do not separate the weak forgetting operator from the standard
forgetting operator. Forgetting in description logics has also been addressed
in [27] via uniform interpolants, where mixed model-theoretic and automata-
theoretic approaches are applied. It is shown that computing uniform
interpolants in the context of the description logics considered, is generally
highly intractable.

Forgetting is particularly useful in rule-based languages, when one simplifies
a belief base to improve querying performance, or protect its parts [20, 30,
31]. This is especially useful for Answer Set Programs, where the
corresponding entailment tasks, centering around necessary conditions, are
typically intractable. In [30] semantic forgetting is proposed. It preserves
skeptical and credulous consequences on unforgotten variables, as well as
strong equivalence of ASP programs. It is shown that computing the forgetting
result is intractable even for Horn logic programs. The paper [20], provides a
comprehensive survey of the area as pertains to Answer Set Programs.

In summary, while the topic of forgetting in knowledge representation has
gained considerable attention with numerous publications, the dual weak
forgetting operator which is proposed and investigated in this paper, has not
been explicitly considered in the literature. Additionally, the fundamental
principles of forgetting founded on the entailment-based, inferential
perspective, which is the starting point of this paper, is somewhat unique in
comparison to other papers, where theoretical results are a consequence of
model-theoretical, or other considerations. This perspective, which results in
entailment preservation on a respective sublanguage, naturally leads to the
consideration of both standard and weak forgetting operators.

Second-order quantifier elimination is used in this paper as the main logical
tool for computing propositional, first-order and fixpoint equivalents of both
standard and weak forgetting operators. Although there are several alternative
techniques that could be used (see, e.g., [19]), Ackermann-like approaches
have been selected for their expressive power and pragmatic application.
Combining Ackermann-like lemmas with tautology-preserving formula
transformations, as exhibited in this paper, has been shown to be very
powerful and useful in many different contexts, including that of computing
dual forgetting operators.

In particular, as shown in [11], the Dls algorithm subsumes most other known
techniques that have been developed for computing circumscription. The paper
[6], shows that the Dls algorithm covers all Sahlqvist formulas, an important
class of formulas used in modal correspondence theory. The fixpoint lemma of
[28], has been used originally for application to modal correspondence theory.
This in turn has led to the development of the Dls* algorithm for fixpoint
computations, which has been used for computing various forms of domain
circumscription [12]. Both the Dls and Dls* algorithms have been shown to be
useful in computing weakest sufficient and strongest necessary conditions
[13]. The previously mentioned works [8, 22, 33], in addition to other papers
by these authors, have shown that Ackermann-like techniques are also powerful
tools for computing forgetting in description logics. The experimental results
of these papers also show that such approaches are very efficient and
applicable to real-world problems. For other uses of Ackermann-like
approaches, including use of the Dls and Dls* algorithms, see [19].

##  8 Conclusions

This paper provides a general characterization of forgetting founded on an
entailment-based, inferential framework. In doing so, an interesting
forgetting operator, weak forgetting, is identified which is dual to the
standard forgetting operator studied in recent work [26]. Due to the
entailment-based, inferential framework presented, it is shown how quantifier
elimination techniques based on Ackermann’s Lemma, using existing algorithms,
$DLS$ and $DLS^{*}$, can be used to compute output of both forgetting
operators. Additionally, the tight relationship between weak forgetting and
weakest sufficient conditions, and standard forgetting and strongest necessary
conditions is characterized in a straightforward manner.

This paper first approaches the topics using the propositional logic case and
then generalizes these results for the first-order and fixpoint logic case,
offering new expressivity in the pragmatic use of such operators. Throughout,
the paper provides examples justifying the introduction of the weak forgetting
operator and also shows how the computational framework is used to derive
inferences from application of both forgetting operators. Similarities and
distinctions between related work and work presented in this paper are
provided. This work opens up a new way to think about forgetting operators and
their pragmatic application in general, by integrating diverse threads of
previous research in this area and new results from this paper, in one
uniform, formal, entailment-based, inferential framework.

Based on this approach, it is also shown in Theorems 3.1(p.3), 3.2(p.2),
6.1(p.3) and 6.2(p.2) that from the perspective of entailment, the operators
$F^{SC}\big{(}\big{)}$ and $F^{NC}\big{(}\big{)}$, generate the formally best
possible (maximal) results of forgetting, as expressed by the restricted
target language in any application.151515See also Figure 2 and the
explanations in Section 3.4.

## References

  * Abiteboul et al. [1995] Abiteboul, S., Hull, R., Vianu, V., 1995.  Foundations of Databases.  Addison-Wesley.
  * Ackermann [1935] Ackermann, W., 1935.  Untersuchungen über das eliminationsproblem der mathematischen logik.  Mathematische Annalen 110, 390–413.
  * Alchourrón et al. [1985] Alchourrón, C., Gärdenfors, P., Makinson, D., 1985.  On the logic of theory change: Partial meet contraction and revision functions.  J. Symb. Log. 50, 510–530.
  * Areces and de Rijke [2000] Areces, C., de Rijke, M., 2000\.  From description to hybrid logics, and back, in: Wolter, F., Wansing, H., de Rijke, M., Zakharyaschev, M. (Eds.), Proc. Advances in Modal Logic 3, pp. 17–36.
  * Beierle et al. [2019] Beierle, C., Kern-Isberner, G., Sauerwald, K., Bock, T., Ragni, M., 2019.  Towards a general framework for kinds of forgetting in common-sense belief management.  Künstliche Intell. 33, 57–68.
  * Conradie [2006] Conradie, W., 2006.  On the strength and scope of DLS.  J. Appl. Non Class. Logics 16, 279–296.
  * van Dalen [2013] van Dalen, D., 2013.  Logic and Structure.  Universitext, Springer.
  * Del-Pinto and Schmidt [2019] Del-Pinto, W., Schmidt, R., 2019\.  Abox abduction via forgetting in ALC, in: The 33rd AAAI Conf. on AI, pp. 2768–2775.
  * Delgrande [2017] Delgrande, J., 2017.  A knowledge level account of forgetting.  J. Artif. Intell. Res. 60, 1165–1213.
  * van Ditmarsch et al. [2009] van Ditmarsch, H., Herzig, A., Lang, J., Marquis, P., 2009\.  Introspective forgetting.  Synth. 169, 405–423.
  * Doherty et al. [1997] Doherty, P., Łukaszewicz, W., Szałas, A., 1997.  Computing circumscription revisited.  J. Automated Reasoning 18, 297–336.
  * Doherty et al. [1998] Doherty, P., Łukaszewicz, W., Szałas, A., 1998.  General domain circumscription and its effective reductions.  Fundam. Informaticae 36, 23–55.
  * Doherty et al. [2001] Doherty, P., Łukaszewicz, W., Szałas, A., 2001.  Computing strongest necessary and weakest sufficient conditions of first-order formulas, in: Nebel, B. (Ed.), Proc. 17th IJCAI, pp. 145–154.
  * Eiter and Kern-Isberner [2019] Eiter, T., Kern-Isberner, G., 2019\.  A brief survey on forgetting from a knowledge representation and reasoning perspective.  Künstliche Intell. 33, 9–33.
  * Fang et al. [2019] Fang, L., Liu, Y., van Ditmarsch, H., 2019.  Forgetting in multi-agent modal logics.  Artif. Intell. 266, 51–80.
  * Feng et al. [2022] Feng, R., Acar, E., Wang, Y., Liu, W., Schlobach, S., Ding, W., 2022.  Computing sufficient and necessary conditions in CTL: A forgetting approach.  Inf. Sci. 616, 474–504.
  * Feng et al. [2023] Feng, R., Wang, Y., Qian, R., Yang, L., Chen, P., 2023\.  Knowledge forgetting in propositional $\mu$-calculus.  Ann. Math. Artif. Intell. , 1–43.
  * Fermé and Hansson [2011] Fermé, E., Hansson, S.O., 2011\.  AGM 25 years: Twenty-five years of research in belief change.  J. of Philosophical Logic 40, 295–331.
  * Gabbay et al. [2008] Gabbay, D., Schmidt, R., Szałas, A., 2008.  Second-Order Quantifier Elimination. Foundations, Computational Aspects and Applications. volume 12 of Studies in Logic.  College Pub.
  * Gonçalves et al. [2021] Gonçalves, R., Knorr, M., Leite, J., 2021.  Forgetting in answer set programming - A survey.  Theory and Practice of Logic Programming , 1–43.
  * Hinman [2005] Hinman, P., 2005.  Fundamentals of Mathematical Logic.  Taylor & Francis.
  * Koopmann et al. [2020] Koopmann, P., Del-Pinto, W., Tourret, S., Schmidt, R., 2020\.  Signature-based abduction for expressive description logics, in: Calvanese, D., Erdem, E., Thielscher, M. (Eds.), Proc. 17th Int. Conf. KR’2020, pp. 592–602.
  * Lang et al. [2003] Lang, J., Liberatore, P., Marquis, P., 2003.  Propositional independence: Formula-variable independence and forgetting.  J. Artif. Intell. Res. 18, 391–443.
  * Lang and Marquis [2010] Lang, J., Marquis, P., 2010\.  Reasoning under inconsistency: A forgetting-based approach.  Artif. Intell. 174, 799–823.
  * Lin [2000] Lin, F., 2000.  On strongest necessary and weakest sufficient conditions, in: Cohn, A., Giunchiglia, F., Selman, B. (Eds.), Proc. 7th Int. Conf. KR’2000, pp. 167–175.
  * Lin and Reiter [1994] Lin, F., Reiter, R., 1994.  Forget it!, in: In Proc. of the AAAI Fall Symp. on Relevance, pp. 154–159.
  * Lutz and Wolter [2011] Lutz, C., Wolter, F., 2011.  Foundations for uniform interpolation and forgetting in expressive description logics, in: Walsh, T. (Ed.), Proc. IJCAI’11, pp. 989–995.
  * Nonnengart and Szałas [1998] Nonnengart, A., Szałas, A., 1998\.  A fixpoint approach to second-order quantifier elimination with applications to correspondence theory, in: Orłowska, E. (Ed.), Logic at Work: Essays Dedicated to the Memory of Helena Rasiowa, Springer Physica-Verlag. pp. 307–328.
  * Peppas [2008] Peppas, P., 2008.  Belief revision, in: van Harmelen, F., Lifschitz, V., Porter, B. (Eds.), Handbook of KR. Elsevier, pp. 317–359.
  * Wang et al. [2013] Wang, Y., Wang, K., Zhang, M., 2013.  Forgetting for Answer Set Programs revisited, in: Rossi, F. (Ed.), Proc. IJCAI’2013, pp. 1162–1168.
  * Zhang and Foo [2006] Zhang, Y., Foo, N., 2006.  Solving logic program conflict through strong and weak forgettings.  Artificial Intelligence 170, 739–778.
  * Zhang and Zhou [2010] Zhang, Y., Zhou, Y., 2010.  Forgetting revisited, in: Lin, F., Sattler, U., Truszczynski, M. (Eds.), Proc. 12th Int. Conf. KR’2010, pp. 602–604.
  * Zhao and Schmidt [2017] Zhao, Y., Schmidt, R., 2017\.  Role forgetting for ALCOQH (universal role)-ontologies using an Ackermann-based approach, in: Sierra, C. (Ed.), Proc. IJCAI’17, pp. 1354–1361.