On the No-Counterexample Interpretation

Ulrich Kohlenbach

December 1997


In [Kreisel 51],[Kreisel 52] G. Kreisel introduced the no-counterexample interpretation (n.c.i.) of Peano arithmetic. In particular he proved, using a complicated tex2html_wrap_inline33-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 tex2html_wrap_inline39 of order type tex2html_wrap_inline41 which realize the Herbrand normal form tex2html_wrap_inline43 of A.

Subsequently more perspicuous proofs of this fact via functional interpretation (combined with normalization) and cut-elimination where found. These proofs however do not carry out the n.c.i. as a local proof interpretation and don't respect the modus ponens on the level of the n.c.i. of formulas A and tex2html_wrap_inline49. Closely related to this phenomenon is the fact that both proofs do not establish the condition tex2html_wrap_inline51 and - at least not constructively - tex2html_wrap_inline53 which are part of the definition of an `interpretation of a formal system' as formulated in [Kreisel 51].

In this paper we determine the complexity of the n.c.i. of the modus ponens rule for

PA-provable sentences,
for arbitrary sentences tex2html_wrap_inline55 uniformly in functionals satisfying the n.c.i. of (prenex normal forms of) A and tex2html_wrap_inline59 and
for arbitrary tex2html_wrap_inline55 pointwise in given tex2html_wrap_inline63-recursive functionals satisfying the n.c.i. of A and tex2html_wrap_inline49.

This yields in particular perspicuous proofs of new uniform versions of the conditions tex2html_wrap_inline69.

Finally we discuss a variant of the concept of an interpretation presented in [Kreisel 58] and show that it is incomparable with the concept studied in [Kreisel 51],[Kreisel 52]. In particular we show that the n.c.i. of PAtex2html_wrap_inline71 by tex2html_wrap_inline73-recursive functionals (tex2html_wrap_inline75) is an interpretation in the sense of [Kreisel 58] but not in the sense of [Kreisel 51] since it violates the condition tex2html_wrap_inline51

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.