Applying G\"odel's Dialectica Interpretation to Obtain a Constructive Proof of Higman's Lemma

TL;DR

This paper employs G"odel's Dialectica interpretation to transform Nash-Williams' non-constructive proof of Higman's Lemma into a concise constructive proof, providing an explicit algorithm for finding embedded pairs in sequences.

Contribution

It introduces a novel application of G"odel's Dialectica interpretation to produce a constructive proof of Higman's Lemma, preserving Nash-Williams' combinatorial insights.

Findings

Constructive proof of Higman's Lemma for decidable well-quasi-orders

Explicit program for finding embedded pairs in sequences

Clarification of Nash-Williams' combinatorial idea in a constructive setting

Abstract

We use G\"odel'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.