Is there any reasonable non-regular Gödel numbering of the language of arithmetic?

Question

Let $\mathcal{L}$ be the language of arithmetic given as follows:

• $x::= {\sf v} \mid x'$
• $t ::= x \mid 0 \mid {\sf S}t \mid (t+t) \mid (t\times t)$
• $A ::= \bot \mid \top \mid t=t \mid \neg A \mid (A \wedge A) \mid (A \vee A) \mid (A \to A) \mid \forall x\,A \mid \exists x\, A$

Definition. Let $\xi$ be a numbering of $\mathcal{L}$. We call $\xi$ regular if for all closed $\mathcal{L}$-terms $u,t$ we have

• $\xi(\mathsf{S}t) > \xi(t) + 1$;
• $\xi((t+u)) > \xi(t) + \xi(u)$;
• $\xi((t \times u)) > \xi(t) \cdot \xi(u)$.

We may reformulate the definition of regularity for alternative reasonable notation systems, such as Polish notation, etc.

Question. Is there any reasonable numbering of $\mathcal{L}$ which is not regular?

The idea is to find such a numbering with a minimum of hacking. It should, as it were, be a numbering someone could come up with without our question in mind. It would be already interesting to know whether this holds for the sub-language of $\mathcal{L}$ which only contains $0$, $\mathsf{S}$ and $\times$.

This question appeared while writing a paper with Albert Visser on Gödel numberings which satisfy the Strong Diagonal Lemma for $\mathcal{L}$ (i.e., without extra function symbols). Clearly, the constraint of regularity (plus monotonicity) rules out such numberings and is satisfied by all standard numberings we are aware of. We wonder whether there are any natural candidates which do not satisfy this constraint?

Answer 1

For the language which contains only $0$, $\mathsf{S}$ and $\times$, one reasonable way to describe a term is by the sequence of strings of esses. E.g. \begin{align} \mathsf{S}0 &\text{ is “one set of one ess"}\\ \mathsf{SS}0\times \mathsf{S}0 &\text{ is “one set of two esses and one set of one ess"}\\ \mathsf{SS}0\times\mathsf{S}0\times \mathsf{S}0 &\text{ is “one set of two esses and two sets of one ess"}\\ \end{align}

Rendering those English-language descriptions as numbers in base 26 gives a numbering scheme $\xi$ for the language. But the example above shows that the scheme is not regular because $$\xi(\mathsf{SS}0\times\mathsf{S}0\times \mathsf{S}0) < \xi(\mathsf{SS}0\times \mathsf{S}0) \cdot \xi(\mathsf{S}0)$$

A similar scheme for $\mathcal{L}$ could also be irregular.

Answer 2

Edit I have read Fedor Pakhomov's comment above and his comment contains all points essential in my answer but in a much compressed form. Indeed, substitutions may be seen as forming a DAG, and Fedor also uses an argument from the rate of growth of iterated squaring vs. the linear length of a term in a DAG-like form. So my answer is rather an elaboration on Fedor's comment. End of edit

Let me provide an example of such a non-regular coding which I believe is not completely ``out of the blue''. The inspiration for it comes from boolean circuits. There, a circuit is called a formula if all its internal nodes have out-degree at most one. This means that we cannot use a function computed by a node more than once. Such a circuit easily translates into a boolean formula of a similar size. I'll do the opposite.

Imagine that while making our Gödel coding we want to be space efficient. So, while computing $\xi(t)$, we want to code efficiently subterms which appear more than once in a term $t$. This corresponds to a situation when we allow arbitrary circuits to code our terms and formulas.

Assume that we want to code a term $t$ which is of the form $t'(s\backslash x)$, where $x$ occurs in $t'$ more than once and $x$ does not occur in $t$. Then, we may represent $t$ as a sequence $(s \rightarrow x)(t')$. Of course, while writing down $t'$ and $s$ we use the same trick recursively. Finally, the obtained sequence of symbols can be coded by any efficient coding of sequences of bits. Let $\xi$ be such a coding. The point is that such a method may decrease the length (and the size) of codes for terms with lots of regularities.

A coding as above is not regular. Let me provide an example. I take a sequence of terms. The term $t_0=2$ and $t_{i+1}=(t_i*t_i)$. The length of the term $t_i$ is $O(2^{i})$ and its the value is $2^{2^{i}}$. On the other hand, the length of a sequence describing $t_i$ with substitutions is $O(i\log_2(i))$ (the $\log_2(i)$ factor comes from the lengths of new variables in the sequence of substitutions). Such a sequence may look like this: $$ (2\rightarrow x_0)(x_0 * x_0\rightarrow x_1)(x_1*x_1\rightarrow x_2)\dots (x_{i-2}*x_{i-2}\rightarrow x_{i-1})(x_{i-1}*x_{i-1}). $$ As the length of this sequence is $O(i\log_2(i))$, the Gödel number for this sequence, $\xi(t_i)$, is of order $2^{O(i\log_2(i))}$.

Let $\text{val}(t)$ be the value of a term $t$. Now, let us assume that $2<\xi(2)$ and let us take $i$ big enough. I claim that it is impossible that $\forall j<i (\xi(t_j)*\xi(t_j)< \xi(t_{j+1}))$. It this would be the case, then for all $j\leq i$ the value of $t_j$ would be less then $\xi(t_j)$. But this is impossible, as the value of $t_i$ is $2^{O(2^i)}$ while $\xi(t_i)$ is $2^{O(i\log_2(i))}$.

PS. The above coding allows to reconstruct $t$ from $\xi(t)$. But $\xi(t)$ depends on the choice of terms $s$ that we substitute. If one would like to make $\xi(t)$ unique, then one should fix this choice. E.g. one could always choose the longest term $s$ which occurs more than once in $t$ and the leftmost one if such $s$ is not unique.

PPS. If we have totality of $\exp$ then the function computing a value of a term from its code is total. However, in models of weak arithmetics (without $\exp$) we may have codes of terms for which ''values'' would be "outside" a model.