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\).