On the no-counterexample interpretation

In [15], [16] G. Kreisel introduced the no-counterexample interpretation (n.c.i.) of Peano arithmetic. In particular he proved, using a complicated epsilon-substitution method (due to W. Ackermann), that for every theorem A (A prenex) of first-order Peano arithmetic PA one can find ordinal recursive functionals <(Phi)under bar>(A) of order type < epsilon(0) which realize the Herbrand normal form A(H) of A. Subsequently more perspicuous proofs of this fact via functional interpretation (combined with normalization) and cut-elimination were found. These proofs however do not carry our the no-counterexample interpretation as a local proof interpretation and don't respect the modus ponens on the level of the no-counterexample interpretation of formulas A and A --> B. Closely related to this phenomenon is the fact that both proofs do not establish the condition (delta) and-at least not constructively-(gamma) which are part of the definition of an 'interpretation of a formal system' as formulated in [15]. In this paper we determine the complexity of the no-counterexample interpretation of the modus ponens rule for (i) PA-provable sentences, (ii) for arbitrary sentences A, B is an element of L(PA) uniformly in functionals satisfying the no-counterexample interpretation of (prenex normal forms of) A and A --> B, and (iii) for arbitrary A, B is an element of L(PA) pointwise in given alpha(< epsilon(0))-recursive functionals satisfying the no-counterexample interpretation of A and A --> B. This yields in particular perspicuous proofs of new uniform versions of the conditions (gamma), (delta). Finally we discuss a variant of the concept of an interpretation presented in [17] and show that it is incomparable with the concept studied in [15], [16]. In particular we show that the no-counterexample interpretation of PA(n) by alpha(< omega(n) (omega))-recursive functionals (n greater than or equal to 1) is an interpretation in the sense of [17] but nor in the sense of [15] since it violates the condition (delta).