Gyesik Lee: Friedman Style Independence Results for Kruskal's Theorem

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 $ATR_0$, 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 $ACA_0+KT$, ! subtheory of the second order arithmetic with the arithmetical comprehension plus Kruskal's theorem, is much stronger than $ATR_0$. They showed that $ACA_0+KT$ has the proof-theoretic strength $\vartheta\Omega^\omega»\Gamma_0$, i.e. $\vartheta\Omega^\omega$ is the smallest ordinal of which well-foundedness can't be proved in $ACA_0+KT$. Here we will investigate the provability of the Friedman-style results in $ACA_0+KT$. The methods used here are invoked by those which A. Weiermann has developed in his papers.

Bibliography

RW93

Michael Rathjen and Andreas Weiermann.
Proof-theoretic investigations on Kruskal's theorem.
Ann. Pure Appl. Logic, 60(1):49-88, 1993.

Sim85

Stephen G. Simpson.
Nonprovability of certain combinatorial properties of finite trees.
In Harvey Friedman's research on the foundations of mathematics, pages 87-117. North-Holland, Amsterdam, 1985.

Wei02

Andreas Weiermann.
An application of graphical enumeration to ${P}{A}$.
To appear in The Journal of Symbolic Logic, 2002.

Back to the Index