David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Journal of Symbolic Logic 64 (4):1491-1511 (1999)
In ,  G. Kreisel introduced the no-counterexample interpretation (n.c.i.) of Peano arithmetic. In particular he proved, using a complicated ε-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 Φ A of order type 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 → B. Closely related to this phenomenon is the fact that both proofs do not establish the condition (δ) and--at least not constructively-- (γ) which are part of the definition of an 'interpretation of a formal system' as formulated in . 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 ∈ 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 ∈ L(PA) pointwise in given α( 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 (γ), (δ). Finally we discuss a variant of the concept of an interpretation presented in  and show that it is incomparable with the concept studied in , . In particular we show that the no-counterexample interpretation of PA n by α( n (ω))-recursive functionals (n ≥ 1) is an interpretation in the sense of  but not in the sense of  since it violates the condition (δ)
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
No references found.
Citations of this work BETA
Paulo Oliva & Thomas Powell (2012). On Spector's Bar Recursion. Mathematical Logic Quarterly 58 (4‐5):356-265.
Ulrich Kohlenbach (2012). Gödel Functional Interpretation and Weak Compactness. Annals of Pure and Applied Logic 163 (11):1560-1579.
Pavol Safarik & Ulrich Kohlenbach (2010). On the Computational Content of the Bolzano-Weierstraß Principle. Mathematical Logic Quarterly 56 (5):508-532.
Similar books and articles
G. Kreisel (1952). On the Interpretation of Non-Finitist Proofs: Part II. Interpretation of Number Theory. Applications. Journal of Symbolic Logic 17 (1):43-58.
Stein Haugom Olsen (2004). Modes of Interpretation and Interpretative Constraints. British Journal of Aesthetics 44 (2):135-148.
Justus Diller (2008). Functional Interpretations of Constructive Set Theory in All Finite Types. Dialectica 62 (2):149–177.
Sergei Tupailo (2001). Realization of Analysis Into Explicit Mathematics. Journal of Symbolic Logic 66 (4):1848-1864.
W. W. Tait (2005). Gödel's Reformulation of Gentzen's First Consistency Proof for Arithmetic: The No-Counterexample Interpretation. Bulletin of Symbolic Logic 11 (2):225-238.
Zlatan Damnjanovic (1995). Minimal Realizability of Intuitionistic Arithmetic and Elementary Analysis. Journal of Symbolic Logic 60 (4):1208-1241.
Added to index2009-01-28
Total downloads5 ( #241,947 of 1,140,268 )
Recent downloads (6 months)1 ( #142,694 of 1,140,268 )
How can I increase my downloads?