Since 2014
On the No-Counterexample Interpretation
BRICS Report Series
View Archive Info| Field | Value | |
| Title |
On the No-Counterexample Interpretation
|
|
| Creator |
Kohlenbach, Ulrich
|
|
| Description |
In [15],[16] Kreisel introduced the no-counterexample interpretation (n.c.i.) of Peanoarithmetic. In particular he proved, using a complicated epsilon-substitution method (due toW. 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 < epsilon_0 which realize theHerbrand normal form A^H of A. Subsequently more perspicuous proofs of this fact via functional interpretation (combinedwith normalization) and cut-elimination were found. These proofs however do not carry out the n.c.i. as a local proof interpretation and don't respect the modusponens on the level of the n.c.i. of formulas A and A -> B. Closely related to this phenomenon is the fact that both proofs do not establish the condition (delta) and - atleast not constructively - (gamma) which are part of the definition of an `interpretation of aformal system' as formulated in [15].In this paper we determine the complexity of the n.c.i. of the modus ponens rule for(i) PA-provable sentences,(ii) for arbitrary sentences A;B in L(PA) uniformly in functionals satisfying the n.c.i. of (prenex normal forms of) A and A -> B; and(iii) for arbitrary A;B in L(PA) pointwise in given alpha(< epsilon_0)-recursive functionals satisfying the n.c.i. 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] andshow that it is incomparable with the concept studied in [15],[16]. In particular we showthat the n.c.i. of PA_n by alpha(= 1) is an interpretation in the sense of [17] but not in the sense of [15] since it violates the condition (delta). |
|
| Publisher |
Aarhus University
|
|
| Date |
1997-06-12
|
|
| Type |
info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion |
|
| Format |
application/pdf
|
|
| Identifier |
https://tidsskrift.dk/brics/article/view/18968
10.7146/brics.v4i42.18968 |
|
| Source |
BRICS Report Series; No 42 (1997): RS-42 On the No-Counterexample Interpretation
BRICS Report Series; Nr. 42 (1997): RS-42 On the No-Counterexample Interpretation 1601-5355 0909-0878 |
|
| Language |
eng
|
|
| Relation |
https://tidsskrift.dk/brics/article/view/18968/16607
|
|