Well quasi-orders and the functional interpretation
Logic
2017-06-12 v1 Logic in Computer Science
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.
Cite
@article{arxiv.1706.02881,
title = {Well quasi-orders and the functional interpretation},
author = {Thomas Powell},
journal= {arXiv preprint arXiv:1706.02881},
year = {2017}
}