Let be r.e. and suppose there is a sentence such that does not prove . Then is more powerful than in two ways:

- It proves
*more*theorems than ; for example, . - It provides
*much shorter*proofs of theorems of ; for example: For any (total) recursive function there is a sentence provable in but such that in there is a proof of such that no proof of in is shorter than .

This leads to considering those recursive functions of which can prove that they are total. One calls such functions *provably recursive* in . It is easy to show that for any -sound , there are recursive functions that are not provably recursive in . The statement that is total,

,

is easily seen to be and for one can provide natural examples of such recursive but not provably recursive functions , thus providing natural (combinatorial) examples of independent -sentences. Actually, this can also be done for much stronger systems than , like , and Harvey Friedman has provided several such examples.

For , the most famous examples are perhaps the following:

- Goodstein (1944). The
*pure base- representation of a number*is obtained by writting in base , writing the exponents of this representation also in base , writing the exponents of these representations in base , and so on. For let and for let be the result of writing the pure base- representation of , replacing each by , and subtracting . The*Goodstein sequence*of is the sequence This sequence eventually converges to*0*. The function that to assigns the number of steps necessary for this to occur is recursive but not provably recursive in . In fact, given any provably recursive in , eventually dominates . - Kirby, Paris (1982). Define a
*hydra*to be a finite rooted tree. A*head*of the hydra is any node (other than the head) with only one edge connected to it,*together*with this edge. Hercules fights the hydra by chopping off its heads one by one by stages. At stage , the hydra grows new heads as follows: from the node that used to be attached to the head just removed, traverse one edge towards the root and from this node just reached, sprout*copies*of the part of the hydra above the edge just traversed. For any hydra, no matter how Hercules battles it, he eventually wins (i.e., the hydra is reduced to a single node). Moreover, given a hydra there is an absolute bound on the number of stages that it takes Hercules to win. Coding (in any reasonable fashion) hydras by numbers, the function that assigns this number to a given hydra is recursive but eventually dominates all functions provably recursive in . - Paris, Harrington (1977). Given a set , let denote the collection of its subsets of size . Given a function , say that a subset of is homogeneous for iff restricted to is constant, and say that it is
*large*if . Ramsey’s theorem, provable in , states that for any there is an such that given any of size , any of size and any , there is a homogeneous for and of size at least . The function that to assigns the least such is well known to be primitive recursive (just about any standard proof of Ramsey theorem in any combinatorics book shows that it roughly grows exponentially). Paris and Harrington showed that if we also require that the homogeneous set be large, then the new statement is also true but the resulting function (clearly recursive) eventually dominates all functions provably recursive in .