Sergei, this is a reply to your comment asking about enumerating formulas in $\mathcal R$. Sorry to post it as a separate answer but I no longer have the browser cookie to post it as a followup comment.
You don't need a particular standardized enumeration, but just some computable mapping between formulas and natural numbers so that each formula gets a unique number. Such a numbering scheme is traditionally called a "Gödel numbering" and the numbers are called "Gödel numbers" because the idea was (I think) introduced in Gödel's landmark paper (1931) about the incompleteness theorem.
A simple Gödel numbering scheme (similar to the one Gödel used) is like this: say the formulas are written in an "alphabet" whose "letters" are $\{\sigma_1,\sigma_2,\ldots\}$. Treat those as natural numbers the obvious way (i.e. $\sigma_k\mapsto k$). So a formula F might be written as $(F_1,F_2,\ldots F_n)$ where the $F_i$ are natural numbers. Then let
$$N_F=2^{F_1}\cdot 3^{F_2} \cdot 5^{F_3} \cdots p_n^{F_n}$$
where $p_i$ is the $i$'th prime number. That is the Gödel number for F (under this particular scheme). It's pretty easy to see how to convert a formula to a number and back. Some numbers won't correspond to valid formulas so treat them as identically zero, for example.
Maybe you should read an introductory book on logic, if you want more clarity about this stuff. There are some other threads suggesting them.
