Well quasi-orders and the functional interpretation

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

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.
Original languageEnglish
Title of host publicationWell-Quasi Orders in Computation, Logic, Language and Reasoning
EditorsPeter Schuster, Monika Seisenberger, Andreas Weiermann
PublisherSpringer International Publishing
Pages221-269
DOIs
Publication statusPublished - 2020

Publication series

NameTrends in Logic
Volume53

Cite this

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