A Worked Example of the Functional Interpretation
Henry Towsner · arXiv (Cornell University) · 2015
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.