FOM: applications of proof theory; combinatorial references
Stephen G Simpson
simpson at math.psu.edu
Wed Apr 1 12:27:29 EST 1998
Steel 25 Mar 1998 10:06:05 asked about "test questions" for
Gentzen-style proof theory.
Traditionally, Gentzen-style proof-theory has been viewed as providing
"consistency proofs" for various subsystems of second order
arithmetic. In my opinion, this is not a very good way to view the
matter, because the ordinal analysis itself (Feferman, Sch"utte,
Takeuti, Feferman-Aczel, Rathjen) is very complicated and therefore
unconvincing with respect to consistency of the systems considered.
To my mind, the most impressive applications of Gentzen-style ordinal
analysis to date have been in the area of combinatorial independence
results. In the early 1980's, Harvey Friedman used ordinal notations
to show that certain mathematically natural finite combinatorial
statements are independent of ATR_0 and Pi^1_1-CA_0. The
combinatorial statements are related to Kruskal's theorem on embedding
finite trees, and a gap-embedding variant, respectively. This is
exposited in one of my papers in the Harvey Friedman volume,
North-Holland, 1985. The original German version of that paper was an
outgrowth of my seminar talk in Munich explaining Harvey's results to
the Munich proof theorists: Pohlers, Buchholz, Sch"utte. That talk
was a great success. Sch"utte especially got quite excited, and a
Sch"utte-Simpson paper was written:
Kurt Sch"utte and Stephen G. Simpson, Ein in der reinen
Zahlentheorie unbeweisbarer Satz "uber endlichen Folgen von
nat"urlichen Zahlen, Archiv fur mathematische Logik und Grundlagen
der Mathematik, 25, 1985, pp. 75-89.
In addition, Gaisi Takeuti eventually wrote up the Kruskal/Friedman
results in the second edition of his book on proof theory,
North-Holland, 1987. The moral of this story is that proof-theorists
of the Sch"utte and Takeuti schools seem to appreciate these
applications to combinatorial independence results.
Afterward, Harvey collaborated with Robertson and Seymour to show that
the graph minor theorem, a very famous and important theorem about
embeddings of finite graphs, is independent of Pi^1_1-CA_0. That
paper appeared in
Stephen G. Simpson (editor), Logic and Combinatorics,
Contemporary Mathematics, Volume 65, American Mathematical
Society, 1987, 384 pages.
Addressing Steel's question, Harvey Friedman 25 Mar 1998 14:13:19
writes:
> The only test questions I know of surround the mysterious highly
> impredicative proofs that are currently used to prove some
> combinatorial theorems. I'm thinking of such things as a) the
> Nash-Williams infinite tree theorem; b) Kriz's theorem answering a
> conjecture of mine about the well quasi ordering of finite trees
> with embeddings with gap condition; c) idempotent ultrafilters and
> a combinatorial theorem of Carlson; d) related theorems from wqo
> and bqo theory e) perhaps also various theorems from ergodic
> theory. ....
Here is some relevant literature.
Papers of Igor Kriz:
Proving a witness lemma in better-quasiordering theory: the method
of "extensions". Math. Proc. Cambridge Philos. Soc. 106 (1989),
no. 2, 253--262.
Well-quasiordering finite trees with gap-condition. Proof of Harvey
Friedman's conjecture. Ann. of Math. (2) 130 (1989), no. 1,
215--226.
The structure of infinite Friedman trees. Adv. Math. 115 (1995),
no. 1, 141--199.
Papers of T. Carlson and S. Simpson:
A dual form of Ramsey's Theorem, Advances in Mathematics, 53, 1984,
pp. 265-290.
Topological Ramsey Theory, in: Mathematics of Ramsey Theory, edited
by J. Nesetril and V. Rodl, Springer-Verlag, 1990, pp. 172-183.
Papers of T. Carlson:
Some unifying principles in Ramsey theory. Discrete Math. 68 (1988),
117-169.
An infinitary version of the Graham-Leeb-Rothschild
theorem. J. Combin. Theory Ser. A 44 (1987), 22-33.
Papers of H. Furstenberg and Y. Katznelson:
A density version of the Hales-Jewett theorem.
J. Anal. Math. 57 (1991), 64--119.
Idempotents in compact semigroups and Ramsey theory.
Israel J. Math. 68 (1989), no. 3, 257--270.
Paper of Richard Shore:
On the strength of Fra"isse's conjecture, Logical Methods,
Birkh"auser, 1993, 813 pages, pp. 782-813.
Papers of Alberto Marcone:
Foundations of BQO Theory and Subsystems of Second
Order {A}rithmetic", Ph. D. thesis, Pennsylvania State University,
1993.
Foundations of BQO theory, Transactions of the American Mathematical
Society, 1994, 345, 641-660.
The set of better quasi orderings is Pi^1_2-complete, Mathematical
Logic Quarterly, 1995, 41, 373-383.
On the logical strength of Nash-Williams' theorem on transfinite
sequences, in: Logic: From Foundations to Applications; European
Logic Colloquium, Clarendon Press, 1996, W. Hodges, M. Hyland,
C. Steinhorn and J. Truss, pp. 327-351.
-- Steve
More information about the FOM
mailing list