CFG emptiness and finiteness are decidable

To decide emptiness, compute the least set of generating variables: start with variables that have a production to a terminal word, and repeatedly add a variable $A$ once some production $A\to \alpha$ has every variable occurring in $\alpha$ already marked generating. Because $V$ is finite, this fixed-point computation halts. By [L1], the language is empty exactly when the start variable $S$ never becomes generating.

For finiteness, first replace $G$ by an equivalent grammar $G^{\mathrm{\prime }}$ using [L2], [L3], and [L4], so that every remaining variable is useful, there are no unit productions, and there are no epsilon-productions except possibly the start-symbol exception. Build the directed dependency graph on the variables of $G^{\mathrm{\prime }}$ with an edge $A\to B$ whenever some production for $A$ contains $B$ on its right-hand side.

If some reachable variable $A$ lies on a directed cycle of this graph, then usefulness gives a terminal derivation from each variable on the cycle, while the removal of unit and nonstart epsilon-productions forces at least one terminal symbol to be added when the cycle is traversed once. Hence there is a derivation $A{\Rightarrow }_{G^{\mathrm{\prime }}}^{\ast }xAy$ with $\mathrm{\mid }xy\mathrm{\mid }\ge 1$. Repeating that cycle any number of times and then finishing to terminals yields words of arbitrarily large length in $L(G^{\mathrm{\prime }})=L(G)$, so the language is infinite.

Conversely, if the reachable part of the dependency graph is acyclic, then no root-to-leaf path in a parse tree can repeat a reachable variable. So parse trees have uniformly bounded depth. Because $G^{\mathrm{\prime }}$ has only finitely many productions and bounded branching, only finitely many parse trees can occur, and therefore only finitely many terminal yields occur. Thus $L(G)$ is finite.

Step 1.1 decides emptiness, and steps 2.1-2.2 decide finiteness by a finite graph-cycle test.