The purpose of this article is to study the role of Gödel’s functional interpretation in the extraction of programs from proofs in well quasi-order theory. The main focus is on the interpretation of Nash–Williams’ famous minimal bad sequence construction, and the exploration of a number of much broader problems which are related to this, particularly the question of the constructive meaning of Zorn’s lemma and the notion of recursion over the non-wellfounded lexicographic ordering on infinite sequences.
CITATION STYLE
Powell, T. (2020). Well Quasi-orders and the Functional Interpretation. In Trends in Logic (Vol. 53, pp. 221–269). Springer Science and Business Media B.V. https://doi.org/10.1007/978-3-030-30229-0_9
Mendeley helps you to discover research relevant for your work.