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.
|Title of host publication||Proceedings Fourth Workshop on Classical Logic and Computation|
|Publication status||Published - 2012|
|Name||Electronic Proceedings in Theoretical Computer Science|
|Publisher||Open Publishing Association|
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