Skip to main content
Log in

An intuitionistic proof of Kruskal’s theorem

  • Published:
Archive for Mathematical Logic Aims and scope Submit manuscript

This is a preview of subscription content, log in via an institution to check access.

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

References

  1. Brouwer, L.E.J.: Points and spaces. Canad. J. Math. 6, 1–17 (1954) also In: L.E.J. Brouwer, Collected Works, Vol.I. Philosophy and Foundations of Mathematics, A. Heyting, (ed.), North Holland Publ. Co., Amsterdam etc., 1975, pp. 522–538

    MATH  Google Scholar 

  2. Coquand, Th.: An analysis of Ramsey’s Theorem. Inf. Comp. 110, 297–304 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  3. Dickson, L.E.: Finiteness of the odd perfect and primitive abundant numbers with n distinct factors. Am. J. Math. 35, 413–426 (1913)

    MATH  Google Scholar 

  4. Gallier, J.H.: What’s so special about Kruskal’s theorem and the ordinal Γ0? A survey of some results in proof theory. Ann. Pure Appl. Logic 53, 199–260 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  5. Gielen, W., de Swart, H., Veldman, W.: The continuum hypothesis in intuitionism. J. Symb. Logic 46, 121–136 (1981)

    MathSciNet  MATH  Google Scholar 

  6. Higman, G.: Ordering by divisibility in abstract algebras. Proc. London Math. Soc. 2, 326–336 (1952)

    MathSciNet  MATH  Google Scholar 

  7. Kleene, S.C., Vesley, R.E.: The Foundations of Intuitionistic Mathematics, Especially in Relation to Recursive Functions. North Holland Publ. Co., Amsterdam etc., 1965

  8. Kreisel, G.: Reports of the Seminar on Foundations of Analysis. Stanford University, 1963

  9. Kruskal, J.B.: Well-quasi-ordering, the tree theorem, and Vazsonyi’s Conjecture. Trans. Am. Math. Soc. 95, 210–225 (1960)

    MATH  Google Scholar 

  10. Kruskal, J.B.: The Theory of Well-Quasi-Ordering: A Frequently Discovered Concept. J. Combinatorial Theory, Series A 13, 297–305 (1972)

    Google Scholar 

  11. Luckhardt, H.: Extensional Gödel Functional Interpretation, a Consistency Proof of Classical Analysis. Lecture Notes in Mathematics, Vol. 306, Springer-Verlag, Berlin etc., 1973

  12. Martin-Löf, P.: Notes on Constructive Mathematics. Almquist and Wiksell, Stockholm, 1970

  13. Murthy, C.R., Russell, J.R.: A constructive proof of Higman’s Lemma. 5th Annual Symposium on Logic in Computer Science, Philadelphia PA. (IEEE Computer Soc. Press, Silver Spring, MD) pp. 257-267

  14. Nash-Williams, C.St.J.A.: On well-quasi-ordering finite trees. Proc. Cambridge Phil. Soc. 59, 833–835 (1963)

    MATH  Google Scholar 

  15. Ramsey, F.P.: On a problem of formal logic. Proc. London Math. Soc. 30, 264–286 (1928)

    MATH  Google Scholar 

  16. Rathjen, M., Weiermann, A.: Proof-theoretic investigations on Kruskal’s theorem. Ann. Pure Appl. Logic 60, 49–88 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  17. Richman, F., Stolzenberg, G.: Well Quasi-Ordered Sets. Adv. Math. 97, 145–153 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  18. Robertson, N., Seymour, P.D.: Graph Minors. IV. Tree-Width and Well-Quasi-Ordering. J. Combinatorial Theory, Series B 48, 227–254 (1990)

    Google Scholar 

  19. Schmidt, D.: Well-Partial Orderings and Their Maximal Order Types. Habilitationsschrift, Heidelberg, 1979

  20. Schütte, K., Simpson, S.G.: Ein in der reinen Zahlentheorie unbeweisbarer Satz über endliche Folgen von natürlichen Zahlen. Arch. Math. Logik 25, 75–89 (1985)

    MathSciNet  Google Scholar 

  21. Seisenberger, M.: Kruskal’s tree theorem in a constructive theory of inductive definitions. In: P. Schuster, U. Berger and H. Osswald, (eds.), Reuniting the Antipodes, Constructive and Nonstandard Views of the Continuum, Proceedings of a Symposium held in San Servolo/Venice, May 16-22, 1999, Kluwer Academic Publishers, Dordrecht etc., 2001, pp. 241–255

  22. Simpson, S.G.: Nonprovability of certain combinatorial properties of finite trees. In: L.A. Harrington et al., (eds.), Harvey Friedman’s research on the foundations of mathematics, Studies in Logic and the foundations of mathematics, Vol. 117, North Holland Publ.Co., Amsterdam etc., 1975, pp. 87–117

  23. Simpson, S.: Ordinal numbers and the Hilbert basis theorem. J. Symb. Logic 53, 961–974 (1988)

    MathSciNet  MATH  Google Scholar 

  24. Troelstra, A.S.: Extended Bar Induction of type zero. In: J. Barwise, H.J. Keisler and K. Kunen, (eds.), The Kleene Symposium, Proc., Madison/Wis. USA, 1978, Studies in Logic and the Foundations of Mathematics, Vol. 101, North Holland Publ. Co., Amsterdam etc., 1980, pp. 277–316

  25. Veldman, W., Bezem, M.: Ramsey’s Theorem and the pigeonhole principle in intuitionistic mathematics. J. London Math. Soc. 47, 193–211 (1993)

    MathSciNet  MATH  Google Scholar 

  26. Veldman, W.: Some intuitionistic variations on the notion of a finite set of natural numbers. In: H.C.M. de Swart and L.J.M. Bergmans, (eds.), Perspectives on Negation, essays in Honour of Johan J. de Iongh on the Occasion of His 80th Birthday, Tilburg University Press, Tilburg, 1995, pp. 177–202

  27. Veldman, W.: On sets enclosed between a set and its double complement. In: A. Cantini et al.,~(eds.), Logic and Foundations of Mathematics, Proceedings Xth International Congress on Logic, Methodology and Philosophy of Science, Florence 1995, Volume III, Kluwer Academic Publishers, Dordrecht etc., 1999, pp. 143–154

  28. Veldman, W.: The Borel Hierarchy and the Projective Hierarchy in Intuitionistic Mathematics. Report No. 0103, Department of Mathematics, University of Nijmegen, 2001

  29. Veldman, W.: Almost the Fan Theorem. Report No. 0113, Department of Mathematics, University of Nijmegen, 2001

  30. Veldman, W.: Bijna de waaierstelling. Nieuw Archief voor Wiskunde, vijfde serie, deel 2, 330–339 (2001)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Wim Veldman.

Additional information

31 October 2001

Rights and permissions

Reprints and permissions

About this article

Cite this article

Veldman, W. An intuitionistic proof of Kruskal’s theorem. Arch. Math. Logic 43, 215–264 (2004). https://doi.org/10.1007/s00153-003-0207-x

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00153-003-0207-x

Navigation