lo.logic - When forcing with a poset, why do we order the poset in the order that we do?

The reason is that in the corresponding Boolean algebra, 0 is less than 1. That is, stronger conditions correspond to lower Boolean values in the Boolean algebra. The trivial condition (which is often the empty function in the cases you mention), corresponds to the element 1 in the Boolean alebra.

We definitely want to regard lower elements of the Boolean algebra as stronger, since they have more implications in the Boolean algebra sense. (After all, 0 = false is surely the strongest assumption you could make, right?)

Meanwhile, you can be comforted by the fact that Shelah and many researchers surrounding him (and a few others) use the alternative forcing-upwards notation. Nevertheless, the forcing-downwards notation is otherwise nearly universal.

This difference in culture sometimes causes some funny problems when authors from opposing camps collaborate. Sometimes a compromise is struck to never officially to use the order explicitly, and to write "stronger than" or "weaker than" in words, rather than take sides. Another alternative is the use the forcing turnstyle symbol itself as the order, but this solution suffers from the fact that it only works when the order is separative.

---

Edit. I looked at Cohen's PNAS 1963 article, and in that article, he does not use the forcing-downwards notation at all. Rather, he uses the containment symbol $supset$ explicitly. Thus, the assumption in the question that Cohen did indeed use the downward-oriented relation may be unwarranted. (Perhaps this view is a little softened by the observation that he consistently uses $supset$ rather than $subset$.)

Here is my theory. In logic and set theory there has been a long-standing tradition of consistently using the relation ≤ in preference to ≥, presumably to avoid the problems associated with mixing up the greater-than less-than order. Perhaps this goes back to Cantor? Now, in the case of forcing, it is usually the case that you have a condition P already, and you want to ask whether there is Q stronger than P with a certain property (one rarely asks for weaker conditions this way). Thus, if you have the downward-oriented relation, you can economically say "there is Q ≤ P such that..." This is just how Cohen's text reads, since he says "there is Q supset P such that ...". Generalizing Cohen's containment order to an arbitrary partial order, one then wants to interpret containment as ≤. And then the further support for this convention arrives with the fact that it agrees with the Boolean algebra order a few years later, so it became standard (except for the Shelah school and a few others).