117b – Some additional remarks on provably recursive functions

There are quite a few examples of natural combinatorial statements not provable in \mbox{\sf PA} other than the ones discussed in lecture. The references listed below present several of them and provide a guide to the existent literature; I especially recommend the beautiful expository paper by Stephen Simpson and in general the whole collection where that paper appeared. I will ask you to abstain from looking at the Kanamori-McAloon paper for the time being, since its main result is the content of the last homework set.

There are at least two `combinatorial’ methods for showing that a function is not provably recursive. One is to use indicators, this technique, due to Paris, requires a bit of model theory, and is the method of the proof you are asked to provide in the homework.

The other method comes from a careful analysis of which functions are provably total in \mbox{\sf PA}. For this, one defines a fast-growing hierarchy of recursive functions. This requires some understanding of the concept of an ordinal. The fast-growing (or Grzegorczyk) hierarchy is defined as follows:

  • F_0(n)=n+1.
  • F_{\alpha+1}(n)=F_\alpha^n(n), where the superindex means iterated n times.
  • F_\lambda(n)=F_{\lambda(n)}(n), if \lambda is limit.

Here, \{\lambda(n): n =0,1,\dots\} is some (natural) sequence converging to \lambda (if you are not aware of ordinals, ignore for the moment what the last clause means).

For example, F_1(n)=2n, F_2(n)=2^n n, F_3(n) grows like a stack of n powers of 2 and F_4(n) grows like an iterated stack of powers of 2, there being n such iterations. It is easy to see that each F_n is primitive recursive and strictly increasing, that n<m implies that F_n is eventually dominated by F_m (i.e., that F_n(k)<F_m(k) for all but finitely many values of k), and that every primitive recursive function is eventually dominated by some F_n. Thus, if a function eventually dominates each F_n, it cannot be primitive recursive.

The ordinals provide us with a method for continuing this sequence while preserving that its members are (eventually) increasing and the sequence itself is increasing under eventual domination. Say that a linearly ordered set X is well-ordered if it has no infinite descending chains. For our purposes, the ordinals are simply a way to talk about well-ordered sets (classically, ordinals denoted the order types of the well-ordered sets, i.e., the equivalence classes of these sets under the relation of being order-isomorphic. The modern viewpoint is different and we don’t need it here). We use n to denote the order type of any linearly ordered set of n elements, and use \omega to represent the order type of the natural numbers. We `add’ two order types \alpha and \beta by forming the disjoint union of a set of order type \alpha followed by a set of order type \beta. We also say that \alpha is smaller than \beta if any set of order type \beta has a (proper) initial segment of order type \alpha. We can then continue the sequence 0,1,2,\dots of the natural numbers, as follows: 

\omega,\omega+1,\omega+2,\dots,\omega 2,\omega 2+1,\dots,\omega 3,\dots,\omega^2,\dots,\omega^3,\dots

where we use \omega2 to represent \omega+\omega, etc, \omega^2 to represent \omega\omega and so on, and we can continue even beyond:

\omega^\omega,\dots,\omega^{\omega^\omega},\dots

Call \epsilon_0 (epsilon-0) the first ordinal \alpha obtained this way such that

\alpha=\omega^\alpha (so \epsilon_0=\omega^{\omega^{\omega^{...}}}).

One can show that any ordinal below \epsilon_0 admits a unique `pure base \omega‘ representation, from which there is a natural way of defining the sequence \{\lambda(n):n=0,1,\dots\} converging to \lambda whenever \lambda is a limit, which means that it is not of the form \alpha+1 for any \alpha. For example,

\omega,\omega 3,\omega^{\omega^2 3+\omega 17+8} 5+\omega^3 2, etc,

are all limits. So, for example, the sequence \{\lambda(n): n =0,1,\dots\} corresponding to \lambda=\omega is just \lambda(n)=n and the corresponding function F_\omega is easily seen to grow as the (diagonal) Ackermann function A(n,n); the sequence corresponding to \lambda=\omega^3 4 is \lambda(n)=\omega^3 3+\omega^2 n, etc. As before, each F_\alpha is (eventually) strictly increasing and if \alpha<\beta then F_\beta eventually dominates F_\alpha. Each F_\alpha, for \alpha<\epsilon_0 (and in fact, for many more \alpha) is recursive.

The relation of this sequence with \mbox{\sf PA} lies in that any function provably recursive in \mbox{\sf PA} is eventually dominated by one of the F_\alpha with \alpha<\epsilon_0. So, one purely combinatorial way of showing that a function is not provably recursive is to show that it eventually dominates each such F_\alpha. This kind of analysis was developed by Solovay and Ketonen.

There are also other ways of relating \mbox{\sf PA} to this number \epsilon_0, and proof theorists have a lot more to say about this relation.

Additional references:

  • Lecture notes on enormous integers, by H. Friedman. (2001)
  • Unprovable theorems,  by H. Friedman. (2005) See www.math.ohio-state.edu/~friedman/manuscripts.html for additional manuscripts and details.
  • Unprovable theorems and fast-growing functions, by S. Simpson. In Logic and combinatorics, S. Simpson, ed. AMS (1987).
  • On Gödel incompleteness and finite combinatorics, by A. Kanamori and K. McAloon. Annals of Pure and Applied Logic 33 (1987), 23-41.

This entry was posted on Wednesday, February 28th, 2007 at 10:49 am and is filed under 117b: Computability theory. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.

2 Responses to 117b – Some additional remarks on provably recursive functions

  1. Separating computational classes and independence « Teaching page says:
    October 11, 2008 at 1:11 pm

    […] could actually lead to their unprovability in certain formal systems, via the identification of fast growing functions. I quote his message below: [FOM] If “NP is not in P/poly” is barely true, then it […]

    Reply
  2. Separating computational classes and independence | A kind of library says:
    September 6, 2017 at 1:47 pm

    […] could actually lead to their unprovability in certain formal systems, via the identification of fast growing functions. I quote his message […]

    Reply

Leave a comment