Applying Gödel's Dialectica Interpretation to Obtain a Constructive Proof of Higman's Lemma

Thomas Powell
(Queen Mary, University of London, United Kingdom)

We use Gödel's Dialectica interpretation to analyse Nash-Williams' elegant but non-constructive "minimal bad sequence" proof of Higman's Lemma. The result is a concise constructive proof of the lemma (for arbitrary decidable well-quasi-orders) in which Nash-Williams' combinatorial idea is clearly present, along with an explicit program for finding an embedded pair in sequences of words.

In Herman Geuvers and Ugo de'Liguoro: Proceedings Fourth Workshop on Classical Logic and Computation (CL&C 2012), Warwick, England, 8th July 2012, Electronic Proceedings in Theoretical Computer Science 97, pp. 49–62.
Published: 9th October 2012.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: