Some of the first properties we learn about forcing notions are the notions of being *atomless* and being *separative*. Usually any kind of analysis of these terms are left out, as “all forcings we care about are atomless and separative”, so this post will be dedicated to taking a slightly closer look at these properties.

Let’s start off by remembering what we’re dealing with.

Definition.A forcing notion is…

atomlessif every condition has two incompatible extensions.separativeif for every , implies that there’s an such that .prunedif every condition has a proper extension.

Starting with atomlessness, the following proposition is the reason why we care about this property.

Proposition.A forcing is atomless iff has no generic filters in .

**Proof.** : If is atomless and is a generic filter, then define . Let be arbitrary. By atomlessness we get two incompatible extensions , so that at least one of them has to be an element of , making dense. But then , a contradiction.

: Assume is an **atom**, meaning that every two extensions of are compatible. Let be the set of all conditions comparable with , which is then a filter since is an atom. It’s also generic since every dense set will contain a condition below . **QED**

This also shows that atomlessness is a forcing invariant: if two forcings are forcing equivalent then either they’re both atomless or neither is. Why we care about separativeness is a bit more elusive. Firstly we *do* have the following:

Theorem.A forcing is separative iff embeds densely into a complete boolean algebra .

**Proof.** is easy to check, so we’ll show . Let a subset be a **cut** if it’s downwards closed with respect to ‘s ordering. To every let . Say that a cut is **regular** if . The topological analogue here is that *cuts are open sets* and *regular cuts are clopen sets*.

Now note that separativity of implies that every is regular. Again, the analogue here is that when we’re dealing with trees then all the basic open sets are clopen. Now simply let be the set of all regular cuts of and note that to every cut there’s a least regular cut containing it; namely,

.

We can therefore let , and . Since any intersection of regular cuts is regular, is complete. We can now define as , which is clearly a dense embedding. **QED**

The only thing separativity is giving us in the above theorem is injectivity of the embedding however, as any forcing is strongly forcing equivalent to a separative one:

Theorem.To every forcing there exists a separative forcing , called theseparative quotient, and a dense order-preserving map such that for all .

**Proof.** Surprisingly, will be a quotient of . We define iff they are compatible with exactly the same things in . This can be shown to be an equivalence relation, so let , which can be shown to be a separative forcing, and the quotient map satisfies the wanted. **QED**

This also shows that *being separative is not a forcing invariant*, in contrast with atomlessness.

As for the relationship between being atomless and being separative, note first of all that every *pruned* separative forcing is atomless. But aside from that we don’t really get any implications between the two:

Proposition.There exists a separative forcing which isn’t atomless, and an atomless forcing which isn’t separative.

**Proof. **For the first bit, let to be the following forcing, which is easily seen to be separative and not atomless:

For the second one, let be the following forcing, which is the union of a full binary tree with an extra element with the following relations:

It’s clearly atomless and note that but any condition below will be compatible with , making it non-separative. **QED**

So, I suppose we can think of the atomless forcings as being the ‘non-trivial ones’, and the separative forcings as the ‘well-behaved ones’. In most cases we’d therefore want both, and we note that being separative *and* atomless is the same thing as being separative and pruned. If we take the boolean algebraic approach to forcing then restricting ourselves to separative pruned forcings would correspond to restricting ourselves to atomless complete boolean algebras, which seems quite reasonable.