### 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 language | English |
---|---|

Title of host publication | Proceedings Fourth Workshop on Classical Logic and Computation |

Pages | 49-62 |

Volume | 97 |

DOIs | |

Publication status | Published - 2012 |

### Publication series

Name | Electronic Proceedings in Theoretical Computer Science |
---|---|

Publisher | Open 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