fully recursive NL/Formula grammar

We need to be able to handle cases like

Let $S = \{ n \in Z | \text{$n$ is even} \}$

where NL contains a formula that contains NL, which contains a formula again.

I guess we need have parallel categories in the NL and F subgrammars, and wherever category NX is allowed also a category FX is allowed.