Why in Laver forcing, the elements of it, i.e. the particular trees are ordered by inverse inclusion? Functions in the Cohen forcing are ordered by ordinary inclusion. (All here is in the Shelah's notation). For the Laver forcing, type
"Laver forcing" inverse inclusion
into google.
I think this is a good question - it gets at the issue of what a forcing condition is "doing" to build the generic object.
First, let's do something pretty general!
A condition in a forcing notion which adds a real (e.g. Cohen, Laver, Mathias, ...) can be thought of as having two parts:
The amount of the real built so far, and
A restriction on how the real is to be built in the future.
The ordering on these conditions, then, has three components, detailing how these two pieces interact (see below for these).
Cohen forcing can be thought of as what you get in the "degenerate" case: the condition is entirely data of the first kind, a finite sequence of zeros and ones.
A non-degenerate example is provided by (say) Mathias forcing, which has a very Ramsey-theoretic flavor: a Mathias condition is a pair $(p, X)$ where
$p$ is a finite set of natural numbers, and
$X$ is an infinite set of natural numbers, each larger than $max(p)$.
The $p$-part is "the amount of the real built so far," and the $X$-part is "the restriction on how the real is to be built in the future.
It will turn out that Laver forcing can also be thought of as a non-degenerate example of such a forcing, and this will lead to the (in my opinion) "right" intuition to have.
Alright, now above we mentioned something about the ordering of conditions having three parts. Let's take a look at how Mathias conditions are ordered, first. We set $(p, X)\le (q, Y)$ ($(p, X)$ is stronger than $(q, Y)$) if
$p\supseteq q$,
$X\subseteq Y$, and
$p\setminus q\subseteq Y$.
Now let's try to give this a general meaning. You'll notice there are three requirements here (as opposed to Cohen's single requirement - remember that Cohen is the degenerate case!). These requirements, intuitively, state respectively that:
(1) The stronger condition builds more of the real ($p\supseteq q$).
(2) The stronger condition places more restrictions on the real, or gives fewer options for the future ($X\subseteq Y$).
(3) Everything "new" that the stronger condition did was allowed by the weaker condition's restrictions ($p\setminus q\subseteq Y$).
Now think back to the Cohen case: there, the restriction was nonexistent, so clauses (2) and (3) don't exist, and all we're left with is normal inclusion for the amount-so-far part. However, in general we do have restrictions, so in general we should expect the ordering to look like usual inclusion on the amount-so-far side and reverse inclusion on the restriction-for-the-future side.
OK, now let's finally look at Laver forcing. The right way to think of Laver forcing is as follows:
Each Laver condition consists of a finite stem $p$ (the amount of the real built so far) and a tree $T$ above that stem (a restriction on how the real can be built in the future) with certain properties.
The tree $T$ restricts the construction of the generic real by saying that, as we continue to grow the stem, we must never leave the tree.
One condition $(p, T)$ is stronger than another $(q, S)$ if $p$ extends $q$, $S$ is contained wholly in $T$, and $p$ is on the tree $T$. Note that this matches exactly the general requirements (1)-(3) above.
It is then a possibly unexpected feature of Laver forcing that we happen to be able to simplify this definition: we can bundle the whole data $(p, T)$ into a single object (the Laver tree), and then (1)-(3) simplify to "the tree gets smaller." But I think this obscures the underlying intuition, which is threefold: the stem gets longer, the tree gets smaller, and the "new" stem is grown entirely in the "old" tree.
So Laver forcing should be thought of as following a general pattern for adding reals, of which Cohen forcing is the "degenerate" case. Once we un-simplify things a bit, the "right" picture emerges.
An incredibly general version of this picture which has proved quite valuable can be found in Shelah's theory of creature forcings; I'm unqualified to discuss it in detail, however.