Prove that $OVERLAP_{CFG}$ is undecidable

Question

Consider the language

$OVERLAP_{CFG} = \{\langle G, H \rangle \mid G \text{ and } H \text{ are CFGs, where } L(G) \cap L(H) \neq \emptyset\}.$

I aim to show that $OVERLAP_{CFG}$ is undecidable.

We can use the reduction method to $A_{TM}$ but I can't figure out how to set up the demonstration (even the TM)

I usually set up problems this way, but with CFG I wouldn't know how to start, for example ...

Let $SO_{TM} = \{ \langle M \rangle \mid M \text{ is a TM with alphabet } \Sigma = \{1,2,\ldots,9\} \text{ that accepts only ordered words} \}$.

The following machine $F$ computes a reduction from $A_{\text{TM}}$ to $SO_{TM}$:

$F$ = "on input $\langle M, w \rangle$, where $M$ is a TM and $w$ is a string:

1. Construct the following machine $M'$:
   On input $x$:

   1. If $x = 111$, accept.
   2. If $x = 211$, execute $M$ on input $w$ and return the same result as $M$.
   3. In all other cases, reject.

2. Return $\langle M' \rangle$.

Answer 1

The set of valid computations of a Turing machine $M$, i.e. strings of the form $q_0w_1\dots w_n\to w_1'q_1w_2\dots w_n\to\dots\to s_1fs_2$ where these are instantaneous descriptions of $M$, $s_1,s_2$ are strings and $f$ is a final state of $M$, is the intersection of two context free languages (think of it as two PDAs, checking the even-to-odd and odd-to-even transitions).

Then, if it is decidable to check that $L(G_1)\cap L(G_2)=\emptyset$, then it is decidable to check if $L(M)$ is empty for any Turing machine $M$. But it is easy to prove that this problem is undecidable - you can invoke Rice's theorem or do it by hand.