Set Builder Notation: POS_λ(\alpha) Explained

[gnome]

How would you describe this set in plain English:
$$\text{POS}_\lambda(\alpha) = \alpha_\lambda^0 \cup \{\kappa - \{\lambda\}|\kappa \in \alpha_\lambda^+\}$$

where:
$\lambda$ is a literal
$\kappa$ is an $\vee$ clause with the set $\kappa = \vee_{j\leq m}\;\lambda_j$ represented as $\kappa = \{\lambda_j|j \leq m \}$
$\{\lambda\}$ is a unit clause consisting of just a single literal $\lambda$
a CNF formula $\alpha$ is a set $\alpha = \wedge_{i\leq n}\;\kappa_i$ represented as $\alpha = \{\kappa_i|i \leq n \}$

a clause $\kappa$ is called $\lambda-positive$ if $\lambda \in \kappa$
a clause $\kappa$ is called $\lambda-negative$ if $\neg \lambda \in \kappa$
a clause $\kappa$ is called $\lambda-neutral$ if $\kappa$ is neither $\lambda-positive$ nor $\lambda-negative$
if $\alpha$ is a set of clauses, $\alpha_\lambda^+$ is the set of $\lambda-positive$ clauses of $\alpha$, $\alpha_\lambda^-$ is the set of $\lambda-negative$ clauses of $\alpha$, and $\alpha_\lambda^0$ is the set of $\lambda-neutral$ clauses of $\alpha$.


At first, I was reading $\text{POS}_\lambda(\alpha)$ as the union of the $\lambda-neutral$ clauses of $\alpha$ with the $\lambda-positive$ clauses of $\alpha$ but excluding the unit clause $\{\lambda\}$. But apparently it is intended to be read as the union of the $\lambda-neutral$ clauses of $\alpha$ with the $\lambda-positive$ clauses of $\alpha$ but with ALL of the $\lambda$ terms EXCLUDED from those clauses.

WHY is it read that way? Or, to put it another way, why was it not written as $\text{POS}_\lambda(\alpha) = \alpha_\lambda^0 \cup \{\kappa - \lambda|\kappa \in \alpha_\lambda^+\}$. (Why did they put their $\lambda$ in brackets {}?) And how would you write set-builder notation for "the $\lambda-positive$ clauses of $\alpha$ but excluding just the unit clause $\{\lambda\}$."

This comes from Computability, Complexity and Languages by Davis, Sigal and Weyuker, section 12.4, discussion of the Davis-Putnam rules for algorithms to manipulate CNF formulas.

 

[Hurkyl]

Bleh, one day I'll learn this terminology.

The expression A - B is the set formed from everything in the set A that is not in the set B. Thus, to "remove" the element λ from the set κ, you have to subtract off the singleton set containing λ.

 

[gnome]

Hmmm...

It becomes surprisingly clear when you put it that way.

Thanks.