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 writing
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
.