Academic Journals Database
Disseminating quality controlled scientific knowledge

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

Author(s): Thomas Powell

Journal: Electronic Proceedings in Theoretical Computer Science
ISSN 2075-2180

Volume: 97;
Issue: Proc. CL;
Start page: 49;
Date: 2012;
Original page

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.
RPA Switzerland

Robotic Process Automation Switzerland


Tango Rapperswil
Tango Rapperswil