A Worked Example of the Functional Interpretation
Logic
2015-03-20 v1
Abstract
The functional interpretation is a systematic, syntactic method for transforming certain non-constructive proofs into constructive proofs with explicit bounds. We illustrate the interpretation by working through a concrete, fairly simple example, with almost no reference to formal logic, and then explain the connection with the underlying proof-theoretic methods.
Keywords
Cite
@article{arxiv.1503.05572,
title = {A Worked Example of the Functional Interpretation},
author = {Henry Towsner},
journal= {arXiv preprint arXiv:1503.05572},
year = {2015}
}