
# 5.9: NUM and SUB Are Representable


In our proof of the Self-Reference Lemma in Section 6.2, we will have to be able to substitute the Gödel number of a formula into a formula. To do this it will be necessary to know that a couple of functions are representable, and in this section we outline how to construct $$\Delta$$-definitions of those functions. First we work with the function $$Num$$.

Recall that $$\bar{a}$$ is the numeral representing the number $$a$$. Thus, $$\bar{2}$$ is $$SS0$$. Since $$SS0$$ is an $$\mathcal{L}_{NT}$$-term, it has a Gödel number, in this case

$\ulcorner SS0 \urcorner = \langle 11, \ulcorner S0 \urcorner \rangle = \langle 11, 2^{12} 3^{1025} \rangle = 2^{12} 3^{2^{12} 3^{1025} + 1}.$

The function $$Num$$ that we seek will map 2 to the Gödel number of its $$\mathcal{L}_{NT}$$ numeral, $$2^{12} 3^{1025} = 2^{12} 3^{2^{12} 3^{1025} + 1}$$. So $$Num \left( a \right) = \ulcorner a \urcorner$$.

To write a $$\Delta$$-definition $$Num \left( a, y \right)$$ we will start, once again, with a construction sequence, but this time we will construct the numeral $$\bar{a}$$ using a particular term construction sequence. To give an example, consider the case $$a = 2$$. We will use the easiest construction sequence that we can think of, namely

$\left( 0, S0, SS0 \right),$

which gives rise to the sequence of Gödel numbers

$\left( \ulcorner 0 \urcorner, \ulcorner S0 \urcorner, \ulcorner SS0 \urcorner \right) = \left( 1024, 2^{12} 3^{1025}, 2^{12} 3^{2^{12} 3^{1025} + 1} \right),$

which is coded by the number

$c = 2^{\left[ 1025 \right]} 3^{\left[ 2^{12} 3^{1025} + 1 \right]} 5^{\left[ 2^{12} 3^{2^{12} 3^{1025} + 1} + 1 \right]}.$

Notice that the length of the construction sequence here is 3, and in general the construction sequence will have length $$a + 1$$ if we seek to code the construction of the Gödel number of the numeral associated with the number $$a$$. (That is a very long sentence, but it does make sense if you work through it carefully.)

You are asked in Exercise 1 to write down the formula

$NumConstructionSequence \left( c, a, y \right)$

as a $$\Delta$$-formula. The idea is that

$\mathfrak{N} \models NumConstructionSequence \left( c, a, y \right)$

if and only if $$c$$ is the code for a construction sequence of length $$a + 1$$ with last element $$y = \ulcorner a \urcorner$$.

Now we would like to define the formula $$Num \left( a, y \right)$$ in such a way that $$Num \left( a, y \right)$$ is true if and only if $$y$$ is $$\ulcorner a \urcorner$$, and as in Section 5.8, the formula $$\left( \exists c \right) NumConstructionSequence \left( c, a, y \right)$$ does not work, as the quantifier is unbounded. So we must find a bound for $$c$$.

If $$\left( c, a, y \right) \in NUMCONSTRUCTIONSEQUENCE$$, then we know that $$c$$ codes a construction sequence of length $$a + 1$$ and $$c$$ is of the form

$c = 2^{\ulcorner t_1 \urcorner + 1} 3^{\ulcorner t_2 \urcorner + 1} \cdots p_{a+1}^{y+1},$

where each $$t_i$$ is a subterm of $$\bar{a}$$. By Lemma 5.8.6 and Lemma 5.8.7, we know that $$\ulcorner t_i \urcorner \leq y$$ and $$p_{a+1} \leq 2^{\left( a + 1 \right)^{\left( a + 1 \right)}}$$, so

$c \leq 2^{y + 1} 3^{y + 1} \ldots p_{a+1}^{y+1} \left( a+1 \: \text{terms} \right) \leq \left( p_{a+1} \right)^{\left( a + 1 \right)^{\left( a + 1 \right) \left( y + 1 \right)}} \leq \left( 2^{\left( a + 1 \right)^{\left( a + 1 \right)}} \right)^{\left( a + 1 \right) \left( y + 1 \right)}.$

This gives us our needed bound on $$c$$. Now we can define

$$Num \left( a, y \right) =$$

$\left( \exists c < \left( \bar{2}^{\left( a + \bar{1} \right)^{\left( a + \bar{1} \right)}} \right)^{\left( a + \bar{1} \right) \cdot \left( y + \bar{1} \right)} \right) NumConstructionSequence \left( c, a, y \right).$

The next formulas that we need to discuss will deal with substitution. We will define two $$\Delta$$-formulas:

1. $$TermSub \left( u, x, t, y \right)$$ will represent substitution of a term for a variable in a term $$\left( u_t^x \right)$$.
2. $$Sub \left( f, x, t, y \right)$$ will represent substitution of a term for a variable in a formula $$\left( \phi_t^x \right)$$.

Specifically, we will show that $$\mathfrak{N} \models TermSub \left( \ulcorner u \urcorner, \ulcorner x \urcorner, \ulcorner t \urcorner, y \right)$$ if and only if $$y$$ is the Gödel number of $$u_t^x$$, where it is assumed that $$u$$ and $$t$$ are terms and $$x$$ is a variable. Similarly, $$Sub \left( \ulcorner \phi \urcorner, \ulcorner x \urcorner, \ulcorner t \urcorner, y \right)$$ will be true if and only if $$\phi$$ is a formula and $$y = \ulcorner \phi_t^x \urcorner$$.

We will develop $$TermSub$$ carefully and outline the construction of $$Sub$$, leaving the details to the reader.

First, let us look at an example. Suppose that $$u$$ is the term $$+ \cdot 0S0x$$. Then a construction sequence for $$u$$ could look like

$\left( 0, x, S0, \cdot 0S0, + \cdot 0S0x \right).$

If $$t$$ is the term $$SS0$$, then $$u_t^x$$ is $$+ \cdot 0S0SS0$$, and we will find a construction sequence for this term in stages.

The first thing we will do is look at the sequence (no longer a construction sequence) that we obtain by replacing all of the $$x$$'s in $$u$$'s construction sequence with $$t$$'s:

$\left( 0, SS0, S0, \cdot 0S0, + \cdot 0S0SS0 \right).$

This fails to be a construction sequence, as the second term of the sequence is illegal. However, if we precede this whole thing with the construction sequence for $$t$$, all will be well (recall that we are allowed to repeat elements in a construction sequence):

$\left( 0, S0, SS0, 0, SS0, S0, \cdot 0S0, + \cdot 0S0SS0 \right).$

So to get all of this to work, we have to do three things:

1. We must show how to change $$u$$'s construction sequence by replacing the occurrences of $$x$$ with $$t$$.
2. We must show how to put one construction sequence in front of another.
3. We must make sure that all of our quantifiers are bounded throughout, so that our final formula $$TermSub$$ is a $$\Delta$$-formula.

So, first we define a formula $$TermReplace \left( c, u, d, x, t \right)$$ such that if $$c$$ is the code for a construction sequence of a term with Gödel number $$u$$, then $$d$$ is the code of the sequence (probably not a construction sequence) that results from replacing each occurrence of the variable with Gödel number $$x$$ by the term with Gödel number $$t$$. In the following definition, the idea is that $$e_i$$ and $$a_i$$ are the entries at position $$i$$ of the sequence coded by $$c$$ and $$d$$, respectively, and if we look at it line by line we see: $$c$$ codes a construction sequence for the term coded by $$u$$, $$d$$ codes a sequence; the lengths of the two sequences are the same; if $$e_i$$ and $$a_i$$ are the $$i^\text{th}$$ entries in sequence $$c$$ and $$d$$, respectively, then $$e_i$$ codes 0 if and only if $$a_i$$ also codes 0; $$e_i$$ codes the successor of a previous $$e_j$$ if and only if $$a_i$$ codes the successor of the corresponding $$a_j$$; and so on.

$$TermReplace \left( c, u, d, x, t \right) =$$

$TermConstructionSequence \left( c, u \right) \land Codenumber \left( d \right) \land \\ \left( \exists l < c \right) \left[ Length \left( c, l \right) \land Length \left( d, l \right) \land \\ \left( \forall i \leq l \right) \left( \forall e_i < c \right) \left( \forall a_i < d \right) \\ \left( \left( IthElement \left( e_i, i, c \right) \land IthElement \left( a_i, i, d \right) \right) \rightarrow \\ \left[ \left( \left[ \left( Variable \left( e_i \right) \land e_i = x \right) \leftrightarrow a_i = t \right] \land \\ \left( Variable \left( e_i \right) \land e_i \neq x \right) \leftrightarrow \left( Variable \left( a_i \right) \land a_i = e_i \right) \right) \land \\ \left( e_i = \bar{2}^{\bar{10}} \leftrightarrow a_i = \bar{2}^{\bar{10}} \right) \land \\ \left( \forall j < i \right) \left[ \left( \left( \exists e_j < c \right) IthElement \left( e_j, j, c \right) \land e_i = \bar{2}^{\bar{12}} \cdot \bar{3}^{e_j} \right) \rightarrow \\ \left( \left( \exists a_j < d \right) IthElement \left( a_j, j, d \right) \land a_i = \bar{2}^{\bar{12}} \cdot \bar{3}^{a_j} \right) \right] \land \\ \vdots \\ \left( \text{Similar clauses for} \: +, \cdot, \: \text{and} \: E. \right) \\ \vdots \\ \right] \right) \right].$

Now that we know how to destroy a construction sequence for $$u$$ by replacing all occurrences of $$x$$ with $$t$$, we have to be able to put a term constructions sequence for $$t$$ in front of our sequence to make it a construction sequence again. So suppose that $$d$$ is the code for the sequence obtained by replacing $$x$$ by $$t$$, and that $$b$$ is the code for the term construction sequence for $$t$$. Essentially, we want $$a$$ to code $$d$$ appended to $$b$$. So the length of $$a$$ is the sum of the lengths of $$b$$ and $$d$$, and the first $$l$$ elements of the $$a$$ sequence should be the same as the $$b$$ sequence, where the length of the $$b$$ sequence is $$l$$, and the rest of the $$a$$ sequence should match, entry by entry, the $$d$$ sequence:

$$Append \left( b, d, a \right) =$$

$Codenumber \left( b \right) \land Codenumber \left( d \right) \land Codenumber \left( a \right) \land \\ \left( \exists l < b \right) \left( \exists m < d \right) \left( Length \left( l, b \right) \land \\ Length \left( m, d \right) \land Length \left( l + m, a \right) \land \\ \left( \forall e < a \right) \left( \forall i \leq l \right) \left[ IthElement \left( e, i, a \right) \leftrightarrow IthElement \left( e, i, b \right) \right] \land \\ \left( \forall e < a \right) \left( \forall j \leq m \right) \left[ 0 < j \rightarrow \\ \left( IthElement \left( e, l+ j, a \right) \leftrightarrow IthElement \left( e, j, d \right) \right) \right] \right).$

Now we are ready to define the formula $$TermSub \left( u, x, t, y \right)$$ that is supposed to be true if and only if $$y$$ is the (Gödel number of the) term that results when you take the term (with Gödel number) $$u$$ and replace (the variable with Gödel number) $$x$$ by (the term with Gödel number) $$t$$. A first attempt at a definition might be

$\left( \exists a \right) \left( \exists b \right) \left( \exists d \right) \left( \exists c \right) \left[ TermConstructionSequence \left( c, u \right) \land \\ TermConstructionSequence \left( b, t \right) \land \\ TermReplace \left( c, u, d, x, t \right) \land Append \left( b, d, a \right) \land \\ TermConstructionSequence \left( a, y \right) \right].$

This is nice, but we need to bound all of the quantifiers. Bounding $$b$$ and $$d$$ is easy: They are smaller than $$a$$. As for $$c$$, we showed when we defined the formula $$Term \left( a \right)$$ that the term coded by $$u$$ must have a construction sequence coded by a number less than $$\left( 2^{u^u} \right)^{u^2 + u}$$. So all that is left is to find a bound on $$a$$. Notice that we can assume that $$b$$ codes a sequence of length less than or equal to $$t$$, the last entry of $$b$$, and similarly, $$c$$ codes a sequence of less than or equal to $$u$$. Since the sequence coded by $$d$$ has the same length as the sequence coded by $$c$$, and as $$a$$ codes $$b$$'s sequence followed by $$d$$'s, the length of the sequence coded by $$a$$ is less than or equal to $$u + t$$. So

$a \leq 2^{e_1} 3^{e_2} \cdots p_{t+u}^y.$

Now we mirror the definition of $$TermConstructionSequence$$. As each entry of $$a$$ can be assumed to be less than or equal to $$y$$, we get

\begin{align} a &\leq 2^y 3^y \ldots p_{t+u}^y \\ &\leq \left[ \left( p_{t+u} \right)^y \right]^{t+u} \\ &\leq \left( \left[ 2^{t+u^{t+u}} \right]^y \right)^{t+u}. \end{align}

So our $$\Delta$$-definition of $$TERMSUB$$ is

$$TermSub \left( u, x, t, y \right) =$$

$\left( \exists a < \left( \left[ \bar{2}^{t+u^{t+u}} \right]^y \right)^{t+u} \right) \left( \exists b < a \right) \left( \exists d < a \right) \left( \exists c < \left( \bar{2}^{u^u} \right)^{u^{\bar{2}} + u} \right) \\ \left[ TermConstructionSequence \left( c, u \right) \land \\ TermConstructionSequence \left( b, t \right) \land TermReplace \left( c, u, d, x, t \right) \land Append \left( b, d, a \right) \land \\ TermConstructionSequence \left( a, y \right) \right].$

Chaff: Garbage cases. What an annoyance. Our claim in the paragraph preceding the definition of $$TermSub$$ that each entry of $$a$$ will be less than or equal to $$y$$ might not be correct if $$y = u_t^x = u$$, so the substitution is vacuous. The reason for this is that the entries of $$a$$ would include a construction sequence for $$t$$, which might be huge, while $$y$$ might be relatively small. For example, we might have $$u = 0$$ and $$t = v_{123456789}$$ and $$x = v_1$$. In Exercise 3 you are invited to figure out the slight addition to the definition of $$TermSub$$ that takes care of this.

Now we outline the construction of the formula $$Sub \left( f, x, t, y \right)$$, which is to be true if $$f$$ is the Gödel number of a formula $$\phi$$ and $$y$$ is $$\ulcorner \phi_t^x \urcorner$$. The idea is to take a formula construction sequence for $$\phi$$ and follow it by a copy of the same construction sequence where we systematically replace the occurrences of $$x$$ with $$t$$'s. You do have to be a little careful in your replacements, though. If you compare Definitions 1.8.1 and 1.8.2, you can see that the rules for replacing variables by terms are a little more complicated in the formula case than in the term case, particularly when you are substituting in a quantified formula. But the difficulties are not too bad.

So if $$b$$ codes the construction sequence for $$\phi$$, if $$d$$ codes the sequence that you get after replacing the $$x$$'s by $$t$$'s, and if $$Append \left( b, d, a \right)$$ holds, then $$a$$ will code up a construction sequence for $$\phi_t^x$$. After you deal with the bounds, you will have a $$\Delta$$-formula along the lines of

$$Sub \left( f, x, t, y \right) =$$

$\left( \exists a < \: \text{Bound} \right) \left( \exists b < a \right) \left( \exists d < a \right) \\ FormulaConstructionSequence \left( b, f \right) \land \\ FormulaReplace \left( b, f, d, x, t \right) \land Append \left( b, d, a \right) \land \\ FormulaConstructionSequence \left( a, y \right).$

## Exercises

1. Write the formula $$NumConstructionSequence \left( c, a, y \right)$$. Make sure that your formula is a $$\Delta$$-formula with the variables $$c$$, $$a$$, and $$y$$ free. [Suggestion: You might want to model your answer on the construction of $$TermConstructionSequence).] 2. Write out the "Similar Clauses" in the definition of \(TermReplace$$.
3. Change the definition of $$TermSub$$ to take care of the problem mentioned in the Chaff following the definition. [Suggestion: The problem occurs only if the substitution is vacuous. So there are two cases. Either $$u$$ and $$y$$ are different, in which case our definition is fine, or $$u$$ and $$y$$ are equal. What do you need to do then? So we suggest that your answer should be a disjunction, something like
$$MyTermSub \left( u, x, t, y \right) =$$
$\left[ \left( u \neq y \right) \land TermSub \left( u, x, t, y \right) \right] \lor \left[ \left( u = y \right) \land \left( \text{Something Brilliant} \right) \right].$
4. Write out the details of the formula $$Sub$$.