This question seems very basic but I cannot seem to find any literature on it.
Let $\mathbb{P}$ be a forcing notion. If $p$ is a condition of $\mathbb{P}$, define the predecessor set of $p$ to be $$\{q \in \mathbb{P} : p \leq_{\mathbb{P}} q \}.$$ Now assume every condition of $\mathbb{P}$ has a finite predecessor set. Is it possible for $\mathbb{P}$ to add no reals? If so, what is an example of such $\mathbb{P}$?
The answer is yes, because every forcing notion is equivalent to a forcing notion with finite predecessors.
Theorem. Every forcing notion is forcing equivalent to a forcing notion with finite conditions, a family of finite sets ordered by (reverse) inclusion. All such forcing notions have the finite-predecessor condition mentioned in the question.
Proof. Consider any forcing notion $\newcommand\P{\mathbb{P}}\P$. Let $\P^*$ be the forcing notion consisting of the finite pointed subsets of $\P$, that is, finite sets $a\subset\P$ such that $a$ has a least element. We order $\P^*$ by $a\leq b$ if and only if $b\subseteq a$. Since a finite set has only finitely many subsets, this will ensure that $\P^*$ has the finite-predecessor condition.
It is easy to see that $\P^*$ projects to $\P$ by mapping every pointed set to its point. So forcing with $\P^*$ adds a generic for $\P$.
Conversely, I claim that forcing with $\P$ adds a generic for $\P^*$. Assume that $G\subset\P$ is $V$-generic, and let $G^*$ consist of the finite pointed subsets of $G$. This is a filter in $\P^*$, since $G$ is a filter in $\P$. This is $V$-generic for $\P^*$, since if $D^*\subset\P^*$ is dense, then let $D$ consist of the least points of any pointed set in $D^*$ — this will be dense in $\P$. So there is some $q\in D$ which is least in some $b\in D^*$ such that $q\in G$. So $b\subset G$ and thus $b\in G^*$ and so $G^*$ meets $D^*$. So $G^*$ is $V$-generic for $\P^*$.
Since $G$ and $G^*$ are easily constructed from each other, we have $V[G]=V[G^*]$, and so these forcing notions are forcing equivalent. $\Box$
Meanwhile, as Monroe mentions in the comments, a drawback of this observation is that the forcing notion $\P^*$ is not generally separative, since pointed sets in $\P$ can use the same least point but be inclusion incomparable, so they will be incomparable in the $\P^*$ order but compatible with exactly the same conditions, violating separativity. I would view it as a natural version of the question to inquire about separative posets with the finite-predecessor property.
