# Well quasi-orders and the functional interpretation

## TL;DR

This paper explores the application of G"odel's functional interpretation to extract programs from proofs involving well quasi-order theory, focusing on Nash-Williams' minimal bad sequence and related constructive questions.

## Contribution

It provides new insights into the constructive content of classical theorems like Zorn's lemma within the framework of well quasi-order theory.

## Key findings

- Interpretation of Nash-Williams' minimal bad sequence construction
- Analysis of the constructive meaning of Zorn's lemma
- Exploration of recursion over non-wellfounded orderings

## Abstract

The purpose of this article is to study the role of G\"odel'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.