FOM: applications of proof theory; combinatorial references

[Stephen G Simpson]

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