A General Constructive Form of Higman's Lemma

In logic and computer science one often needs to constructivize a theorem for all f there exists g.P ( f, g), stating that for every infinite sequence f there is an infinite sequence g such that P( f, g). Here P is a computable predicate but g is not necessarily computable from f. In this paper we propose the following constructive version of for all f there exists g P (f, g): for every f there is a "long enough" finite prefix g(0) of g such that P(f, g(0)), where "long enough" is expressed by membership to a bar which is a free parameter of the constructive version. Our approach with bars generalises the approaches to Higman's lemma undertaken by CoquandFridlender, Murthy-Russell and Schwichtenberg-Seisenberger-Wiesnet. As a first test for our bar technique, we sketch a constructive theory of well-quasi orders. This includes yet another constructive version of Higman's lemma: that every infinite sequence of words has an infinite ascending subsequence. As compared with the previous constructive versions of Higman's lemma, our constructive proofs are closer to the original classical proofs.