Δ1 bootstrapping


This proves that a number of useful relationsMathworldPlanetmathPlanetmath and functions are Δ1 in first order arithmetic, providing a bootstrapping of parts of mathematical practice into any system including the Δ1 relations (since the Δ1 relations are exactly the recursive ones, this includes Turing machinesMathworldPlanetmath).

First, we want to build a tupling relation which will allow a finite setsMathworldPlanetmath of numbers to be encoded by a single number. To do this we first show that R(a,b)a|b is Δ1. This is true since a|bcb(ac=b), a formulaMathworldPlanetmathPlanetmath with only bounded quantifiers.

Next note that P(x)x is prime is Δ1 since P(x)¬y<x(¬y=1y|x). Also AP(x,y)P(x)P(y)z<y(x<z¬P(x)).

These two can be used to define (the graph of) a primality function, p(a)=a+1-th prime. Let p(a,b)=cba2(¬[2|c][q<brb(AP(q,r)j<c[qj|crj+1|c])][ba|c]¬[ba+1|c]).

This rather awkward looking formula is worth examining, since it illustrates a principle which will be used repeatedly. c is intended to be a function of the form 203152 and so on. If it includes ba but not ba+1 then we know that b must be the a+1-th prime. The definition is so complicated because we cannot just say, as we’d like to, p(a+1) is the smallest prime greater than p(a) (since we don’t allow recursive definitions). Instead we embed the series of values this recursion would take into a single number (c) and guarantee that the recursive relationship holds for at least a terms; then we just check if the a-th value is b.

Finally, we can define our tupling relation. Technically, since a given relation must have a fixed arity, we define for each n a function x0,,xn=npixi+1. Then define (x)i to be the i-th element of x when x is interpreted as a tuple, so (x)0,,(x)n=x. Note that the tupling relation, even taken collectively, is not total. For instance 5 is not a tuple (although it is sometimes convenient to view it as a tuple with “empty spaces”: _,_,5). In situations like this, and also when attempting to extract entries beyond the length, (x)i=0 (for instance, (5)0=0). On the other hand there is a 0-ary tupling relation, =1.

Thanks to our definition of p, we have x0,,xn=xx=p(0)x0+1p(n)xn+1. This is clearly Δ1. (Note that we don’t use the as above, since we don’t have that, but since we have a different tupling function for each n this isn’t a problem.)

For the reverse, (x)i=y([p(i)y+1|x]¬[p(i)y+2|x])([y=0]¬[p(i)|x]).

Also, define a length function by len(x)=y¬[p(y+1)|x]zy[p(z)|x] and a membership relation by in(x,n)i<len(x)[(x)i=n].

Armed with this, we can show that all primitive recursive functionsMathworldPlanetmath are Δ1. To see this, note that x=0, the zero function, is trivially recursive, as are x=Sy and pn,m(x1,,xn)=xm.

The Δ1 functions are closed under compositionMathworldPlanetmath, since if ϕ(x) and ψ(x) both have no unboundedPlanetmathPlanetmath quantifiers, ϕ(ψ(x)) obviously doesn’t either.

Finally, suppose we have functions f(x) and g(x,m,n) in Δ1. Then define the primitive recursion h(x,y) by first defining:

h¯(x,y)=zln(z)=yi<y[(z)i+1=g(x,i,(z)i)][ln(z)=0(z)0=f(x)

and then h(x,y)=(h¯(x,y))y.

Δ1 is also closed under minimization: if R(x,y) is a Δ1 relation then μy.f(x,y) is a function giving the least y satisfying R(x,y). To see this, note that μy.f(x,y)=zf(x,z)m<z¬f(x,m).

Finally, using primitive recursion it is possible to concatenate sequencesMathworldPlanetmath. First, to concatenate a single number, if s=x0,xn then s*1y=tp(len(s)+1)y+1. Then we can define the concatenationMathworldPlanetmath of s with t=y0,,ym by defining f(s,t)=s and g(s,t,j,i)=j*1(t)i, and by primitive recursion, there is a function h(s,t,i) whose value is the first j elements of t appended to s. Then s*t=h(s,t,len(t).

We can also define *u, which concatenates only elements of t not appearing in s. This just requires defining the graph of g to be g(s,t,j,i,x)[in(s,(t)i)x=j][¬in(s,(t)i)x=j*1(t)i]

Title Δ1 bootstrapping
Canonical name Delta1Bootstrapping
Date of creation 2013-03-22 12:58:25
Last modified on 2013-03-22 12:58:25
Owner Henry (455)
Last modified by Henry (455)
Numerical id 10
Author Henry (455)
Entry type Example
Classification msc 03B10