Estoy leyendo esto sección del libro "A Friendly Introduction to Mathematical Logic" de Christopher Leary y Lars Kristiansen. Los autores definen el sistema de codificación como sigue:
La función $\ulcorner \cdot \urcorner$ siendo el dominio la colección de cadenas finitas de $\mathcal{L}_{NT}$ -símbolos y codominio $\mathbb{N}$ se define como sigue:
$$\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}$$
Observe que cada símbolo está asociado a su número de símbolo, tal y como se indica en la tabla
$$\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}$$
Es bastante evidente que este sistema de codificación asigna fórmulas muy pequeñas como $=00$ números muy grandes. En este caso, $\ulcorner =00 \urcorner =2^83^{1025}5^{1025}$ . En lugar de utilizar este sistema de codificación, podríamos simplemente codificar la fórmula $\phi =c_1c_2\ldots c_n$ donde cada $c_i$ es un símbolo (y debe ser uno de los anteriores como en la tabla) de la siguiente manera: $$\ulcorner \phi \urcorner = \prod_{i=1}^{n} p_i ^ {\text{value corresponding to } c_i \text{ in the table}}$$ donde $p_i$ es el i-ésimo primo.
Este mapeo también codificaría fórmulas, pero asignaría fórmulas más pequeñas a números (¡relativamente!) más pequeños. Por ejemplo, $\ulcorner =00 \urcorner = 2^73^95^9$ en mi sistema de codificación.
¿Por qué los autores han elegido el sistema de codificación de la forma en que lo han hecho? ¿Facilita las cosas más adelante? Entiendo que no habría una forma única de hacerlo. Sería estupendo entender por qué se prefieren unos sistemas a otros.
