[FOM] 180:Provable Functions of PA

[Harvey Friedman]

The provably recursive functions of PA have been well studied and are 
well understood. They are the <epsilon_0 recursive functions.

For the purposes of this posting, we will assume that PA has been 
formulated with primitive recursive function symbols. Also, here the 
Sigma_n and Pi_n formulas are those with n alternating quantifiers 
starting with an existential and universal quantifier, followed by a 
quantifier free matrix. The Delta_0, Sigma_0, Pi-0 formulas, are the 
quantifier free formulas.

In the general framework of this posting, the provably recursive 
functions of PA are the functions f:N into N which are given by a 
provable sentence in PA of the form

(forall n)(therexists unique m)(therexists r)(A(n,m,r))

where A is quantifier free.

I.e., the f:N into N such that there is a sentence of that form, 
provable in PA, for which f is the unique outer Skolem function.

More generally, for a natural class K of formulas, we wish to 
consider those f:N into N which are given by a provable sentence in 
PA of the form

(forall n)(therexists unique m)(A(n,m))

where A is in K.

We call such a function a PA provable K function. Thus the provably 
recursive functions of PA are the PA provable Sigma_1 functions.

If we omit the requirement that the sentence above is provable in PA, 
then we say that such a function is a K function. Thus the recursive 
functions are the Sigma_1 functions.

THEOREM 1. (Obvious). The Delta_0 characteristic functions are 
exactly the primitive recursive characteristic functions.

THEOREM 2. The PA provable Delta_0 functions are exactly the Delta_0 
functions that are bounded by a <epsilon_0 recursive function.

We now consider the PA provable Sigma_2 functions. The Sigma_2 
functions are exactly the functions that are recursive in 0'. These 
are also the same as the Delta_2 functions.

The first thing to realize is this.

THEOREM 3. Any recursive function is a PA provable Sigma_2 function.

This can be sharpened as follows.

THEOREM 4. Any function whose graph is a Boolean combination of r.e. 
sets, is a PA provable Sigma_2 function.

Now for the characterization.

THEOREM 5. The PA provable Sigma_2 functions are exactly the 
functions that are <epsilon_0 recursive in some Pi_1 function. In 
particular, we can use the function H(n) = the number of steps it 
takes for the n-th Turing machine to converge at the empty input tape 
if it exists; 0 otherwise.

More generally, we have the following.

THEOREM 6. Let k >= 1. The PA provable Sigma_k functions are exactly 
the functions that are <epsilon_0 recursive in some Pi_k-1 function.

*********************************************

I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 180th in a series of self contained numbered postings to 
FOM covering a wide range of topics in f.o.m. The list of previous 
numbered postings #1-149 can be found at 
http://www.cs.nyu.edu/pipermail/fom/2003-May/006563.html  in the FOM 
archives, 5/8/03 8:46AM. Previous ones counting from #150 are:

150:Finite obstruction/statistics  8:55AM  6/1/02
151:Finite forms by bounding  4:35AM  6/5/02
152:sin  10:35PM  6/8/02
153:Large cardinals as general algebra  1:21PM  6/17/02
154:Orderings on theories  5:28AM  6/25/02
155:A way out  8/13/02  6:56PM
156:Societies  8/13/02  6:56PM
157:Finite Societies  8/13/02  6:56PM
158:Sentential Reflection  3/31/03  12:17AM
159.Elemental Sentential Reflection  3/31/03  12:17AM
160.Similar Subclasses  3/31/03  12:17AM
161:Restrictions and Extensions  3/31/03  12:18AM
162:Two Quantifier Blocks  3/31/03  12:28PM
163:Ouch!  4/20/03  3:08AM
164:Foundations with (almost) no axioms, 4/22/0  5:31PM
165:Incompleteness Reformulated  4/29/03  1:42PM
166:Clean Godel Incompleteness  5/6/03  11:06AM
167:Incompleteness Reformulated/More  5/6/03  11:57AM
168:Incompleteness Reformulated/Again 5/8/03  12:30PM
169:New PA Independence  5:11PM  8:35PM
170:New Borel Independence  5/18/03  11:53PM
171:Coordinate Free Borel Statements  5/22/03  2:27PM
172:Ordered Fields/Countable DST/PD/Large Cardinals  5/34/03  1:55AM
173:Borel/DST/PD  5/25/03  2:11AM
174:Directly Honest Second Incompleteness  6/3/03  1:39PM
175:Maximal Principle/Hilbert's Program  6/8/03  11:59PM
176:Count Arithmetic  6/10/03  8:54AM
177:Strict Reverse Mathematics 1  6/10/03  8:27PM
178:Diophantine Shift Sequences  6/14/03  6:34PM
179:Polynomial Shift Sequences/Correction  6/15/03  2:24PM

Harvey Friedman