5.9: NUM and SUB Are Representable
( \newcommand{\kernel}{\mathrm{null}\,}\)
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 Δ-definitions of those functions. First we work with the function Num.
Recall that ˉa is the numeral representing the number a. Thus, ˉ2 is SS0. Since SS0 is an LNT-term, it has a Gödel number, in this case
⌜SS0⌝=⟨11,⌜S0⌝⟩=⟨11,21231025⟩=212321231025+1.
The function Num that we seek will map 2 to the Gödel number of its LNT numeral, 21231025=212321231025+1. So Num(a)=⌜a⌝.
To write a Δ-definition Num(a,y) we will start, once again, with a construction sequence, but this time we will construct the numeral ˉ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
(0,S0,SS0),
which gives rise to the sequence of Gödel numbers
(⌜0⌝,⌜S0⌝,⌜SS0⌝)=(1024,21231025,212321231025+1),
which is coded by the number
c=2[1025]3[21231025+1]5[212321231025+1+1].
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(c,a,y)
as a Δ-formula. The idea is that
N⊨NumConstructionSequence(c,a,y)
if and only if c is the code for a construction sequence of length a+1 with last element y=⌜a⌝.
Now we would like to define the formula Num(a,y) in such a way that Num(a,y) is true if and only if y is ⌜a⌝, and as in Section 5.8, the formula (∃c)NumConstructionSequence(c,a,y) does not work, as the quantifier is unbounded. So we must find a bound for c.
If (c,a,y)∈NUMCONSTRUCTIONSEQUENCE, then we know that c codes a construction sequence of length a+1 and c is of the form
c=2⌜t1⌝+13⌜t2⌝+1⋯py+1a+1,
where each ti is a subterm of ˉa. By Lemma 5.8.6 and Lemma 5.8.7, we know that ⌜ti⌝≤y and pa+1≤2(a+1)(a+1), so
c≤2y+13y+1…py+1a+1(a+1terms)≤(pa+1)(a+1)(a+1)(y+1)≤(2(a+1)(a+1))(a+1)(y+1).
This gives us our needed bound on c. Now we can define
Num(a,y)=
(∃c<(ˉ2(a+ˉ1)(a+ˉ1))(a+ˉ1)⋅(y+ˉ1))NumConstructionSequence(c,a,y).
The next formulas that we need to discuss will deal with substitution. We will define two Δ-formulas:
- TermSub(u,x,t,y) will represent substitution of a term for a variable in a term (uxt).
- Sub(f,x,t,y) will represent substitution of a term for a variable in a formula (ϕxt).
Specifically, we will show that N⊨TermSub(⌜u⌝,⌜x⌝,⌜t⌝,y) if and only if y is the Gödel number of uxt, where it is assumed that u and t are terms and x is a variable. Similarly, Sub(⌜ϕ⌝,⌜x⌝,⌜t⌝,y) will be true if and only if ϕ is a formula and y=⌜ϕxt⌝.
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 +⋅0S0x. Then a construction sequence for u could look like
(0,x,S0,⋅0S0,+⋅0S0x).
If t is the term SS0, then uxt is +⋅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:
(0,SS0,S0,⋅0S0,+⋅0S0SS0).
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):
(0,S0,SS0,0,SS0,S0,⋅0S0,+⋅0S0SS0).
So to get all of this to work, we have to do three things:
- We must show how to change u's construction sequence by replacing the occurrences of x with t.
- We must show how to put one construction sequence in front of another.
- We must make sure that all of our quantifiers are bounded throughout, so that our final formula TermSub is a Δ-formula.
So, first we define a formula TermReplace(c,u,d,x,t) 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 ei and ai 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 ei and ai are the ith entries in sequence c and d, respectively, then ei codes 0 if and only if ai also codes 0; ei codes the successor of a previous ej if and only if ai codes the successor of the corresponding aj; and so on.
TermReplace(c,u,d,x,t)=
TermConstructionSequence(c,u)∧Codenumber(d)∧(∃l<c)[Length(c,l)∧Length(d,l)∧(∀i≤l)(∀ei<c)(∀ai<d)((IthElement(ei,i,c)∧IthElement(ai,i,d))→[([(Variable(ei)∧ei=x)↔ai=t]∧(Variable(ei)∧ei≠x)↔(Variable(ai)∧ai=ei))∧(ei=ˉ2¯10↔ai=ˉ2¯10)∧(∀j<i)[((∃ej<c)IthElement(ej,j,c)∧ei=ˉ2¯12⋅ˉ3ej)→((∃aj<d)IthElement(aj,j,d)∧ai=ˉ2¯12⋅ˉ3aj)]∧⋮(Similar clauses for+,⋅,andE.)⋮])].
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(b,d,a)=
Codenumber(b)∧Codenumber(d)∧Codenumber(a)∧(∃l<b)(∃m<d)(Length(l,b)∧Length(m,d)∧Length(l+m,a)∧(∀e<a)(∀i≤l)[IthElement(e,i,a)↔IthElement(e,i,b)]∧(∀e<a)(∀j≤m)[0<j→(IthElement(e,l+j,a)↔IthElement(e,j,d))]).
Now we are ready to define the formula TermSub(u,x,t,y) 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
(∃a)(∃b)(∃d)(∃c)[TermConstructionSequence(c,u)∧TermConstructionSequence(b,t)∧TermReplace(c,u,d,x,t)∧Append(b,d,a)∧TermConstructionSequence(a,y)].
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(a) that the term coded by u must have a construction sequence coded by a number less than (2uu)u2+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≤2e13e2⋯pyt+u.
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
a≤2y3y…pyt+u≤[(pt+u)y]t+u≤([2t+ut+u]y)t+u.
So our Δ-definition of TERMSUB is
TermSub(u,x,t,y)=
(∃a<([ˉ2t+ut+u]y)t+u)(∃b<a)(∃d<a)(∃c<(ˉ2uu)uˉ2+u)[TermConstructionSequence(c,u)∧TermConstructionSequence(b,t)∧TermReplace(c,u,d,x,t)∧Append(b,d,a)∧TermConstructionSequence(a,y)].
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=uxt=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=v123456789 and x=v1. 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(f,x,t,y), which is to be true if f is the Gödel number of a formula ϕ and y is ⌜ϕxt⌝. The idea is to take a formula construction sequence for ϕ 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 ϕ, if d codes the sequence that you get after replacing the x's by t's, and if Append(b,d,a) holds, then a will code up a construction sequence for ϕxt. After you deal with the bounds, you will have a Δ-formula along the lines of
Sub(f,x,t,y)=
(∃a<Bound)(∃b<a)(∃d<a)FormulaConstructionSequence(b,f)∧FormulaReplace(b,f,d,x,t)∧Append(b,d,a)∧FormulaConstructionSequence(a,y).
Exercises
- Write the formula NumConstructionSequence(c,a,y). Make sure that your formula is a Δ-formula with the variables c, a, and y free. [Suggestion: You might want to model your answer on the construction of \(TermConstructionSequence).]
- Write out the "Similar Clauses" in the definition of TermReplace.
- 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(u,x,t,y)=
[(u≠y)∧TermSub(u,x,t,y)]∨[(u=y)∧(Something Brilliant)]. - Write out the details of the formula Sub.