Hostname: page-component-586b7cd67f-rdxmf Total loading time: 0 Render date: 2024-11-26T02:43:43.589Z Has data issue: false hasContentIssue false
  • English
  • Français

On the No-Counterexample Interpretation

Published online by Cambridge University Press:  12 March 2014

Ulrich Kohlenbach
Ulrich Kohlenbach*
Affiliation:
BRICS, (Basic Research in Computer Science, Centre of the Danish National Research Foundation), Department of Computer Science, University of Aarhus, NY Munkegade, BLDG. 540, DK.-8000 Aarhus C, Denmark, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

In [15], [16] 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 of order type < ε0 which realize the Herbrand normal form AH 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 nocounterexample 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 [15].

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 64 , Issue 4 , December 1999 , pp. 1491 - 1511
Copyright
Copyright © Association for Symbolic Logic 1999

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Ackermann, W., Zur Widerspruchsfreiheit der reinen Zahlentheorie, Mathematische Annalen, vol. 117 (1940), pp. 162–194.CrossRefGoogle Scholar
[2]Buchholz, H., Feferman, S., Pohlers, W., and Sieg, W., Iterated inductive definitions and subsystems of analysis: Recent proof-theoretical studies, Lecture Notes in Mathematics, vol. 897, Springer, Berlin–Heidelberg–New York, 1981.Google Scholar
[3]Damnjanovic, Z., Minimal readability, this Journal, vol. 60 (1995), pp. 1208–1241.Google Scholar
[4]Feferman, S., Theories of finite type related to mathematical practice, Handbook of mathematical logic (Barwise, J., editor), North-Holland, Amsterdam, 1977, pp. 913–972.CrossRefGoogle Scholar
[5]Feferman, S., Kreisel's ‘Unwinding Program’, Kreiseliana: about and around Georg Kreisel (Odifreddi, P., editor), A.K. Peters, Wellesley Massachusetts, 1996, pp. 247–273.Google Scholar
[6]Girard, J.-Y., Proof theory and logical complexity, Vol. I, Bibliopolis (Napoli) and Elsevier Science Publishers (Amsterdam), 1987.Google Scholar
[7]Gödel, K., Vortrag bei Zilsel, 1938, with English translation in [9], pp. 86–113.Google Scholar
[8]Gödel, K., Über eine bisher noch nicht benütze Erweiterung des finiten Standpunktes, Dialectica, vol. 12 (1958), pp. 280–287.CrossRefGoogle Scholar
[9]Gödel, K., Collected works, Vol III, unpublished essays and lectures, Oxford University Press, New York, 1995.Google Scholar
[10]Howard, W.A., Functional interpretation of bar induction by bar recursion, Compositio Mathematica, vol. 20 (1968), pp. 107–124.Google Scholar
[11]Howard, W.A., Ordinal analysis of bar recursion of type zero, Compositio Mathematica, vol. 42 (1981), pp. 105–119.Google Scholar
[12]Howard, W.A., Ordinal analysis of simple cases of bar recursion, this Journal, vol. 46 (1981), pp. 17–30.Google Scholar
[13]Howard, W.A. and Kreisel, G., Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis, this Journal, vol. 31 (1966), pp. 325–358.Google Scholar
[14]Kleene, S.C., Recursive functionals and quantifiers of finite types I, Transactions of the American Mathematical Society, vol. 91 (1959), pp. 1–52.Google Scholar
[15]Kreisel, G., On the interpretation of non-finitist proofs, part I, this Journal, vol. 16 (1951), pp. 241–267.Google Scholar
[16]Kreisel, G., On the interpretation of non-finitist proofs, part II: Interpretation of number theory, applications, this Journal, vol. 17 (1952), pp. 43–58.Google Scholar
[17]Kreisel, G., Mathematical significance of consistency proofs, this Journal, vol. 23 (1958), pp. 155–182.Google Scholar
[18]Kreisel, G., Functions, ordinals, species, Proceeding of 3rd International Congress, Amsterdam, 1968, pp. 145–159.Google Scholar
[19]Kreisel, G., A survey of proof theory, this Journal, vol. 33 (1968), pp. 321–388.Google Scholar
[20]Kreisel, G. and Levy, A., Reflection principles and their use for establishing the complexity of axiomatic systems, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 14 (1968), pp. 97–142.CrossRefGoogle Scholar
[21]Parsons, C., Proof-theoretic analysis of restricted induction schemata, this Journal, vol. 36 (1971), p. 361.Google Scholar
[22]Parsons, C., On n-quantifier induction, this Journal, vol. 37 (1972), pp. 466–482.Google Scholar
[23]Scarpellini, B., A model for bar recursion of higher types, Compositio Mathematica, vol. 23 (1971), pp. 123–153.Google Scholar
[24]Schwichtenberg, H., Einige Anwendungen von unendlichen Termen und Wertfunktionalen, Habilitationsschrift, Münster, 1973.Google Scholar
[25]Schwichtenberg, H., Proof theory: some applications of cut-elimination, Handbook of mathematical logic (Barwise, J., editor), North-Holland, Amsterdam, 1977, pp. 867–895.CrossRefGoogle Scholar
[26]Schwichtenberg, H., On bar recursion of types 0 and 1, this Journal, vol. 44 (1979), pp. 325–329.Google Scholar
[27]Sieg, W. and Parsons, C., Introductory note to *1938a (‘Vortrag bei Zilsels’), [9], pp. 62–85.CrossRefGoogle Scholar
[28]Spector, C., Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics, Recursive function theory (Dekker, J.C.E., editor), Proceedings of Symposia in Pure Mathematics, vol. 5, American Mathematical Society, Providence, Rhode Island, 1962, pp. 1–27.CrossRefGoogle Scholar
[29]Tait, W.W., The substitution method, this Journal, vol. 30 (1965), pp. 175–192.Google Scholar
[30]Tait, W.W., Normal derivability in classical logic, The syntax and semantics of infinitary languages (Barwise, J., editor), Springer, Berlin, 1968, pp. 204–236.CrossRefGoogle Scholar
[31]Troelstra, A.S. (editor), Metamathematical investigation of intuitionistic arithmetic and analysis, Springer Lecture Notes in Mathematics, vol. 344, 1973.CrossRefGoogle Scholar