Skip to main content
3 of 3
deleted 1 character in body
Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 239

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:

  1. Cohen forcing

  2. 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).

  3. 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.

Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 239