DIALECTICA INTERPRETATION WITH FINE COMPUTATIONAL CONTROL

The functional “Dialectica ” interpretation was developed by Gödel [3] to trans-late classical arithmetic into a quantifier-free system with higher finite types. It can be viewed as an extension of (modified) realisability [7] that allows tracking of terms, which are used to instantiate universal premises of implications. In this way we are able to find witnesses for proofs of weak existence that derive a con-tradiction from the assumption ∀x¬A. Tracking computational content of all open assumptions in a proof is a demanding bookkeeping process. The size of the wit-nesses can grow exponentially, unless special care is taken to factor out common repeated subterms, which helps to reclaim a linear dependency of the the witness size on the proof size [4]. In addition, a case distinction over the quantifier-free Dialectica translation of an assumption formula is required whenever two different uses of the same assumption are encountered. Automatic extraction seems very useful in order to analyse non-trivial examples, but extracted programs could be quite complicated. A careful analysis shows that, just as in the case of realisability (see [1]), th