I am reading this section from the book "A Friendly Introduction to Mathematical Logic" by Christopher Leary and Lars Kristiansen. The authors define the coding system as follows:
The function $\ulcorner \cdot \urcorner$, with domain the collection of finite strings of $\mathcal{L}_{NT}$-symbols and codomain $\mathbb{N}$, is defined as follows:
$$\ulcorner s \urcorner = \begin{cases} \begin{array}{ll} \langle 1, \ulcorner \alpha \urcorner \rangle & \text{if} \: s \: \text{is} \: \left( \neg \alpha \right), \: \text{where} \: \alpha \: \text{is an} \: \mathcal{L}_{NT} \text{-formula} \\ \langle 3, \ulcorner \alpha \urcorner, \ulcorner \beta \urcorner \rangle & \text{if} \: s \: \text{is} \: \left( \alpha \lor \beta \right), \: \text{where} \: \alpha \: \text{and} \: \beta \: \text{are} \: \mathcal{L}_{NT} \text{-formulas} \\ \langle 5, \ulcorner v_i \urcorner, \ulcorner \alpha \urcorner \rangle & \text{if} \: s \: \text{is} \: \left( \forall v_i \right) \left( \alpha \right), \: \text{where} \: \alpha \: \text{is an} \: \mathcal{L}_{NT} \text{-formula} \\ \langle 7, \ulcorner t_1 \urcorner, \ulcorner t_2 \urcorner \rangle & \text{if} \: s \: \text{is} \: = t_1 t_2, \: \text{where} \: t_1 \: \text{and} \: t_2 \: \text{are terms} \\ \langle 9 \rangle & \text{if} \: s \: \text{is} \: 0 \\ \langle 11, \ulcorner t \urcorner \rangle & \text{if} \: s \: \text{is} \: St, \: \text{with} \: t \: \text{a term} \\ \langle 13, \ulcorner t_1 \urcorner, \ulcorner t_2 \urcorner \rangle & \text{if} \: s \: \text{is} \: + t_1 t_2, \: \text{where} \: t_1 \: \text{and} \: t_2 \: \text{are terms} \\ \langle 15, \ulcorner t_1 \urcorner, \ulcorner t_2 \urcorner \rangle & \text{if} \: s \: \text{is} \: \cdot t_1 t_2, \: \text{where} \: t_1 \: \text{and} \: t_2 \: \text{are terms} \\ \langle 17, \ulcorner t_1 \urcorner, \ulcorner t_2 \urcorner \rangle & \text{if} \: s \: \text{is} \: E t_1 t_2, \: \text{where} \: t_1 \: \text{and} \: t_2 \: \text{are terms} \\ \langle 19, \ulcorner t_1 \urcorner, \ulcorner t_2 \urcorner \rangle & \text{if} \: s \: \text{is} \: < t_1 t_2, \: \text{where} \: t_1 \: \text{and} \: t_2 \: \text{are terms} \\ \langle 2i \rangle & \text{if} \: s \: \text{is the variable} \: v_i \\ 3 & \text{otherwise.} \end{array} \end{cases}$$
Notice that each symbol is associated with its symbol number, as set out in the table
$$\begin{array}{||c|c||c|c||} \hline \text{Symbol} & \text{Symbol Number} & \text{Symbol} & \text{Symbol Number} \\ \hline \neg & 1 & + & 13 \\ \lor & 3 & \cdot & 15 \\ \forall & 5 & E & 17 \\ = & 7 & < & 19 \\ 0 & 9 & ( & 21 \\ S & 11 & ) & 23 \\ & & v_i & 2i \\ \hline \end{array}$$
It's quite evident that this coding system assigns very small formulas like $=00$ very large numbers. In this case, $\ulcorner =00 \urcorner =2^83^{1025}5^{1025}$. Instead using this coding system, we could just code formula $\phi =c_1c_2\ldots c_n$ where each $c_i$ is a symbol (and it must be one of the above as in the table) in the following way: $$\ulcorner \phi \urcorner = \prod_{i=1}^{n} p_i ^ {\text{value corresponding to } c_i \text{ in the table}}$$ where $p_i$ is the ith prime.
This mapping would also code formulas but would assign smaller formula to (relatively!!) smaller numbers. For instance, $\ulcorner =00 \urcorner = 2^73^95^9$ in my coding system.
Why did the authors choose their coding system the way they have done? Does it make things easier later? I understand that there would no unique way of doing this. It would be great if I understand why some systems are preferred to others.
As Mauro Allegranza commented, unnecessarily large values is not a drawback. Meanwhile there is a minor advantage that the given system has over prime factorization coding: namely, it makes the syntactic form of the formula more obvious from its code.
Specifically, suppose I give you a number $n$ and tell you that $n$ is the Godel number of a formula $\varphi$, and ask whether $\varphi$ has the form $(\psi\vee\theta)$ or not. Using prime factorization coding this is a bit tricky, since we need to "locate" the prime corresponding to the outermost logical operation. The coding provided in the text, however, makes this trivial: just ask whether $n$ has the form $\langle 3,a,b\rangle$. This makes things a bit simpler when for example defining "$x$ is (the code for) a proof of the sentence (coded by) $y$."