Schwichtenberg, Helmut; Seisenberger, Monika; Wiesnet, Franziskus
(2016):
Higman's Lemma and Its Computational Content.
In:
Advances in Proof Theory. Progress in Computer Science and Applied Logic, Vol. 28. Cham: Birkhäuser. pp. 353375

Full text not available from 'Open Access LMU'.
Abstract
Higman's Lemma is a fascinating result in infinite combinatorics, with manyfold applications in logic and computer science. It has been proven several times using different formulations and methods. The aim of this paper is to look at Higman's Lemma from a computational and comparative point of view. We give a proof of Higman's Lemma that uses the same combinatorial idea as NashWilliams' indirect proof using the socalled minimal bad sequence argument, but which is constructive. For the case of a two letter alphabet such a proofwas given by Coquand. Using more flexible structures, we present a proof that works for an arbitrary wellquasiordered alphabet. We report on a formalization of this proof in the proof assistant Minlog, and discuss machine extracted terms (in an extension of Godel's system T) expressing its computational content.