Well quasi-orders and the functional interpretation

Research output: Chapter or section in a book/report/conference proceedingChapter or section

5 Citations (SciVal)


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
Publication statusPublished - 2020

Publication series

NameTrends in Logic


Dive into the research topics of 'Well quasi-orders and the functional interpretation'. Together they form a unique fingerprint.

Cite this