This definition is sound since the ordering in which literals of L are considered does not matter 4 . We can also prove that the definition above is equivalent to the one in which Point 2. is replaced by ForgetLit(Σ, {l}) = Σι ← 1 V (¬ ∧ Σι ←o)
just because Σ and Σι ← 0 are equivalent modulo ¬ l .

Let us now give a semantical characterization of literal forgetting. If L = { l }, that is, L
is composed of a single literal, then forgetting l from a formula Σ amounts to introducing the model Force(ω, ¬ l) for each model ω of Σ such that ω |= l.

Proposition 14 The set of models of ForgetLit(E,{l}) can be expressed as:
Mod(ForgetLit(Σ,{{})) =

$$\begin{array}{r c l}{{t\left(\Sigma,\{l\}\right)}}&{{=}}&{{M o d(\Sigma)\cup\{F o r c e(\omega,-l)\mid\omega\models\Sigma\}}}\\ {{}}&{{=}}&{{\{\omega\mid F o r c e(\omega,l)\mid=\Sigma\}}}\end{array}$$

A similar statement can be given for the case in which L is composed of more than one literal. In this case, for each model ω of Σ, we can force any subset of literals L 1 ⊆ L such that ω |= L 1 to assume the value false.

Proposition 15 The set of models of ForgetLit(E, L) can be expressed as:
Mod(ForgetLit(Σ, L)) = {ω | Force(ω, L 1 ) |= Σ where L 1 ⊆ L}
As a corollary, we obtain the following properties of literal forgetting:
Corollary 2  Let Σ, Φ be formulas from PROPps and L 1, L 2 ⊆ Lps.

- ∑ |= ForgetLit(Σ, L 1 ) holds. - If Σ |= Φ holds, then ForgetLit(Σ, L 1 ) |= ForgetLit(Φ, L 1 ) holds as well. - If L 1 C L 2 holds, then ForgetLit(E, L 1 ) |= ForgetLit(E, L 2 ) holds as well.

Let now consider an example.

Example 11 Let Σ = (¬a Vb) Λ (α Vc). We have ForgetLit(Σ, {¬a}) ≡ (α Vc) ∧ (bVc).

The key proposition for the notion of forgetting is the following one:
4. The proof of this statement is almost straightforward: let l 1 , l 2 be two literals;