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$.