# An inference in counting branch lengths in a Gödel numbering system

Set up

I'm reading a text where formulae are numbered in the following way. First there is a numbering function $\nu$ such that all logical particles (truth-functional operators and quantifiers, are congruent to some fixed $i$ mod 5). In the author's choice, $\nu(\neg)=0, \nu(\rightarrow)=5$ and so on with some arbitrary choices all divisible by 5. For variable $v_n$ we map $\nu(v_n)=5n+1$. After that we assign $\underline{0}$, the numeral meant to represent the number 0, and $\approx$, the symbol meant to represent equality of terms. Then the arithmetic operations.

$$\nu(\underline{0})=2,\qquad \nu(\approx)=3\\ \nu({\bf s})=4,\ \nu(+)=9,\ \nu(\cdot)=14$$

The Gödel number of a term or formula is then regarded as a list. The following defines the Gödel number for terms, in order of variables, the unique constant $\underline{0}$, successor, plus, and times.

$$GN(v_n) = \langle \nu(v_n)\rangle,\ GN(\underline{0})=\langle\nu(\underline{0})\rangle,\ GN({\bf s}(t)) = \langle \nu({\bf s}),GN(t)\rangle \\ GN(t_1+t_2)=\langle \nu(+),GN(t_1),GN(t_2)\rangle\\ GN(t_1\cdot t_2)=\langle \nu(\cdot),GN(t_1),GN(t_2)\rangle$$

Hence every term is coded in a tree structure of nested lists. We typically use $x$ for the code number of any list of numbers and $y$ for an index in the list, and $(x)_y$ for the number encoded in the $y$th place. We use formulae to represent numbers and numbers to encode lists. We have a defined length function,$\ell(x)$, and $th(y,x)$ function so that $\ell(x)$ is the length of list $x$ and $th(y,x)$ is the $y$th coordinate of $x$ and each of these are represented by some formula. $(x)_y$ is just convenient notation for $th(y,x)$.

Question

The author says that, in any given term tree, encoded by $x$ which is a nested list of lists, and for any coordinate $y$, we have $(x)_y<x$ and therefore as we go down a branch the Gödel number of any term decreases. Ok, that I get by nature of how we've defined the construction of lists.

Next let $t$ be the Gödel number of some term. The author says that, since at every leaf of the tree we have atomic terms with Gödel number > 0, then every branch must have length $< t$. This is the part I don't quite get. I could imagine justifying the conclusion some other way, but I don't see how the given justification is adequate (or even really relevant).

Imagine that you had a branch of length $k \ge t$. This means that $$((\cdots((t)_{y_1})_{y_2}\cdots)_{y_{k-1}})_{y_k}$$ for some $y_i$s, is the encoding of a leaf symbol.
But then we have $$(t)_{y_1} < t \\ ((t)_{y_1})_{y_2} < (t)_{y_1} \\ (((t)_{y_1})_{y_2})_{y_3} < ((t)_{y_1})_{y_2} \\ \vdots$$ which, puts together, gives us $$(t)_{y_1} \le t-1 \\ ((t)_{y_1})_{y_2} \le t-2 \\ (((t)_{y_1})_{y_2})_{y_3} \le t-3 \\ \vdots \\ ((\cdots((t)_{y_1})_{y_2}\cdots)_{y_{k-1}})_{y_k} \le t-k \le 0$$ But no leaf (except $\neg$ which is not allowed in term trees anyway) is represented by a number $\le 0$, so this is a contradiction.