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.
|Title of host publication||Well-Quasi Orders in Computation, Logic, Language and Reasoning|
|Editors||Peter Schuster, Monika Seisenberger, Andreas Weiermann|
|Publisher||Springer International Publishing|
|Publication status||Published - 2020|
|Name||Trends in Logic|
Powell, T. (2020). Well quasi-orders and the functional interpretation. In P. Schuster, M. Seisenberger, & A. Weiermann (Eds.), Well-Quasi Orders in Computation, Logic, Language and Reasoning (pp. 221-269). [Chapter 9] (Trends in Logic; Vol. 53). Springer International Publishing. https://doi.org/10.1007/978-3-030-30229-0_9