Applying Gödel's Dialectica interpretation to obtain a constructive proof of Higman's lemma

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.
Original languageEnglish
Title of host publicationProceedings Fourth Workshop on Classical Logic and Computation
Pages49-62
Volume97
DOIs
Publication statusPublished - 2012

Publication series

NameElectronic Proceedings in Theoretical Computer Science
PublisherOpen Publishing Association
ISSN (Print)2075-2180

Cite this

Powell, T. (2012). Applying Gödel's Dialectica interpretation to obtain a constructive proof of Higman's lemma. In Proceedings Fourth Workshop on Classical Logic and Computation (Vol. 97, pp. 49-62). (Electronic Proceedings in Theoretical Computer Science). https://doi.org/10.4204/EPTCS.97