FINDING DIALECTICA REALISERS FOR AXIOMS

Gödel’s functional (Dialectica) interpretation [1, 6, 9] was designed to translate a possibly non-constructive system to a constructive quantifier-free system employing the concept of primitive recursive functionals of higher finite type. More precisely, each arithmetic formula ϕ translates to a formula ∃x∀yϕD(x, y), such that ϕ is provable in the original system if and only if the quantifier-free ϕD(t, y) is provable in the target constructive system, with t a term (not containing y freely) called the realiser for ϕ. The Dialectica interpretation can be naturally used for program extraction from classical proofs, since its soundness proof provides as with an algorithm to convert a classical proof of the original formula to a realiser and a constructive proof of its translation. One of the main disadvantages of Dialectica, compared to other approaches for program extraction (e.g. Friedman’s A-translation [5] as well as Berger, Buchholz and Schwichtenberg’s refined variant [2]), is that extracted terms tend to become long very fast when the length of the formula increases. The underlying reason for this is that Dialectica was designed to take into accoun