On the No-Counterexample Interpretation
Kohlenbach, Ulrich
J. Symbolic Logic, Tome 64 (1999) no. 1, p. 1491-1511 / Harvested from Project Euclid
In [15], [16] G. Kreisel introduced the no-counterexample interpretation (n.c.i.) of Peano arithmetic. In particular he proved, using a complicated $\varepsilon$-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_A$ of order type < $\varepsilon_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 out 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 $\rightarrow$ 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 $\in \mathscr{L}$(PA) uniformly in functionals satisfying the no-counterexample interpretation of (prenex normal forms of) A and A $\rightarrow$ B, and (iii) for arbitrary A, B $\in \mathscr{L}$(PA) pointwise in given $\alpha$(<$\varepsilon_0$) -recursive functionals satisfying the no-counterexample interpretation of A and A $\rightarrow$ 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 $\geq$ 1) is an interpretation in the sense of [17] but not in the sense of [15] since it violates the condition ($\delta$).
Publié le : 1999-12-14
Classification: 
@article{1183745932,
     author = {Kohlenbach, Ulrich},
     title = {On the No-Counterexample Interpretation},
     journal = {J. Symbolic Logic},
     volume = {64},
     number = {1},
     year = {1999},
     pages = { 1491-1511},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183745932}
}
Kohlenbach, Ulrich. On the No-Counterexample Interpretation. J. Symbolic Logic, Tome 64 (1999) no. 1, pp.  1491-1511. http://gdmltest.u-ga.fr/item/1183745932/