Here we exposit some examples of mathematically meaningful theorems of
finite combinatorics which are unprovable in certain logical
systems. The unprovable combinatorial theorems are concerned with
embedability properties of finite trees. S.G. Simpson in his article,
"Nonprovability of certain combinatorial properties of finite trees",
presents some proof-theoretic results, due to H. Friedman, about
embedability properties of finite trees. Friedman's methods are based
in part on the existence of a close relationship between finite trees
on the one hand, and systems of ordinal notations which occur in
Gentzen-style proof theory on the other. It is shown that both
Kruskals's theorem and its miniaturization are too strong to be
provable in the theory , fragment of the second order
arithmetic with the arithmetical transfinite recursion. Actually it is
shown by M. Rathjen and A. Weiermann in "Proof-theoretic investigation
on Kruskal's theorem" that
, ! subtheory of the second
order arithmetic with the arithmetical comprehension plus Kruskal's
theorem, is much stronger than
. They showed that
has the proof-theoretic strength
,
i.e.
is the smallest ordinal of which
well-foundedness can't be proved in
. Here we will
investigate the provability of the Friedman-style results in
. The methods used here are invoked by those which
A. Weiermann has developed in his papers.