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.