Formal Definition of Finite Conditions Forcing with finite conditions is a common concept used by set theorists. I was thinking about its meaning, but I couldn't find any exact definition of it. At the first glance it seemed to me that maybe by finite conditions, experts mean that the conditions of a forcing notion are finite however one can naturally turn any arbitrary forcing to another one which are isomorphic as partial orders and the conditions of former are finite. On the other hand, the conditions of many forcings with finite conditions are  intrinsically infinite.
By the way implicitly, forcing with finite conditions means every condition has finitely many information about generic object(from forcing point of view). My question is:


Is there any formal definition of forcing with finite condition? Or can some one give a formal definition of forcing with finite condition including well-known forcings with finite conditions?


 A: My impression is that this term is used loosely, without formal definition, to refer to the common situation where we have a forcing notion consisting of a partial order whose elements are all finite functions (that is, each on a finite domain) and the forcing order is functional extension. The most canonical example is Cohen forcing $\text{Add}(\omega,1)$ to add a Cohen real or actually any number of Cohen reals. Other examples include the forcing to collapse a given cardinal to $\omega$ or the forcing to add a club set using finite conditions (not with countable conditions, which is another common way to do it). In some cases, there are examples where conditions are augmented with some other finite amount of information that still counts as forcing with finite conditions even though the order isn't literally functional extension.
Every forcing notion is equivalent, of course, to a forcing notion whose conditions are all finite, since we could replace any element $p$ in a partial order with $\{p\}$, which is a singleton set and hence finite, and then redefine the corresponding order on these singletons. So every condition in the new partial order is finite. But this literal interpretation is never what is meant by the phrase, "forcing with finite conditions," and I have never seen a formal definition of the concept going significantly beyond the loose understanding given in the previous paragraph. 
A: It might be the case that the definition of finite elements from domain theory is what you are looking for. It makes precise the idea that an element of a poset carries finite amount of information.

Definition: Let $(P, {\leq})$ be a poset. An element $x \in P$ is finite (or compact) if it is inaccessible by directed suprema: if $D \subseteq P$ is directed and $x \leq \sup D$ then $x \leq y$ for some $y \in D$.

This is a purely order-theoretic characterization of finiteness and is therefore immune to changes in the presentation of $P$.
Looking at the list of forcing notions, it seems that the following have the property that all elements of the forcing poset are finite:


*

*Cohen forcing

*Levy collapsing of an uncountable cardinal $\lambda$ to $\omega$ (but not the collapsing of $\lambda$ to $\kappa$ when $\kappa$ is uncountable – although in this case we get the related notion of $\kappa$-finiteness).

*Shooting a club with countable conditions.
I have not checked all the other notions, but they generally seem to contain some elements that are non-finite.
In domain theory it usually does not matter so much that a poset consists of only finite elements, but rather that every element is the supremum of finite elements below it. This is known as algebraicity of the poset. Speaking somewhat off the top of my head, I would propose the following:

Tentative definition: A $B$-valued model has finite conditions if the complete Boolean algebra $B$ is algebraic (every element is the supremum of finite elements below it). A forcing notion $P$ has finite conditions if the associated complete Boolean algebra is algebraic.

There is going to be a characterization of a $P$ with finite conditions in the above sense which is intrinsic to $P$ (and certainly if $P$ only has finite elements then it will satisfy the condition). But before working out the details of that, I'd prefer to hear from the experts if the suggestion seems plausibly useful.
