I read somewhere that the problem which asks whether or not a CFG $G$ generates $1^*$ is decidable. The proof goes like this:
$1^* \cap L(G)$ is context free since it is the intersection of a regular language and a CFL, therefore we can test if $1^* \cap L(G)$ is empty since it is decidable to check if the language produced by a CFG is empty. If $1^* \cap L(G)$ is empty, reject, otherwise, accept.
I have doubts however with this proof since it only shows that some string in $1^*$ is generated by $G$, but not whether $G$ generates all strings in $1^*$.
Moreover, if this proof is correct, we can use the same proof outline under the alphabet $\Sigma=\{0,1\}$ to show that $G$ generates $\Sigma^*$, or that $\Sigma^* \subseteq G$. However, it is known that it is undecidable whether $R \subseteq G$, where $R$ is a regular language, and $G$ is a CFG (by setting $R=\Sigma^*$, and $\Sigma=\{0,1\}$.
But to show that a CFG generates $1^*$ is decidable, the only way I can think of is to use something similar to the proof that it is decidable for a PCP instance to generate some string in $1^*$ (i.e., $w=v$, where $w,v \in 1^*$), i.e. we can check if the CFG has rule $S \rightarrow S1$, then accept. Otherwise, if it has rules of the form $S \rightarrow 1^aS1^b$ such that $a > b$, and rules of the form $S \rightarrow 1^cS1^d$ such that $c < d$, then accept... But is there a simpler way to solve this problem?
