A Worked Example of the Functional Interpretation

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.

References in corpus (3)

• Local stability of ergodic averages
• Nonexpansive iterations in uniformly convex $W$-hyperbolic spaces
• An Inverse Ackermannian Lower Bound on the Local Unconditionality Constant of the James Space

Cited by in corpus (1)

• An Inverse Ackermannian Lower Bound on the Local Unconditionality Constant of the James Space