A complexity analysis of functional interpretations (Q557798)

In the Dialectica paper, Gödel gave the following functional interpretation: Given a proof of \(A\) in HA, he associated a formula \(\exists x\forall yA_D (x,y)\) and terms \(t(y)\), where \(A_D\) and \(t(y)\) are in his system T, and \(x,y\) etc. are tuples, and he gave a proof of \(A_D(t(y),y)\) in T. Namely, Skolem functions are given as higher-order terms. Interpretations need not be confined to HA and T. In this paper, the authors take up in a broader context, quantitative questions: How complex terms \(t(y)\) must be, including the structures of the types involved, and how do proof depths compare between \(A\) and \(A_D(t(y),y)\), etc. The authors use \(\text{EIL}^\omega\) -- extended intuitionistic logic of all finite types -- as the basic interpreting theory (i.e., it takes the place of T), and give careful estimates of the complexities in the interpretations of \(\text{EIL}^\omega\) itself, \(\text{EIL}^\omega\) strengthened by new axioms like the Markov principle, the axiom of choice, etc. Then, they work on classical theories, using the double-negation technique. Another pair of theories the authors consider is \(\text{PRA}^\omega\) and its intuitionistic version \(\text{PRA}_{\text i}^\omega\). They construct an algorithm that gives, from a proof of \(\forall x\exists yA_0(x,y)\) in \(\text{PRA}+\text{AC}_0+\text{WKL}\), terms \(t\) and a proof of \(\forall xA_0(x,t(x))\) in \(\text{PRA}_{\text i}^\omega\), eliminating \(\text{AC}_0\) and WKL. (The subscript `0' indicates `quantifier free'.) Of course complexity measure are given, but too elaborate to quote here. A new aspect is given by a monotone interpretation that looks for terms \(t\) such that \(\exists x[t\,\text{maj}\,x\land\forall yA_D(x,y)]\) is proved, instead of \(\forall yA_D(t(y),y)\) itself. The advantage is that this is easier and faster, particularly in handling contraction rules. Due to the nature of the subject, a huge battery of measuring devices is mobilized. The authors' analyses are meticulous and thorough. A big bibliography and guide to it are provided.