Hostname: page-component-6bf8c574d5-nvqbz Total loading time: 0 Render date: 2025-03-11T03:05:22.090Z Has data issue: false hasContentIssue false
  • English
  • Français

A survey of proof theory

Published online by Cambridge University Press:  12 March 2014

G. Kreisel
G. Kreisel*
Affiliation:
Stanford University
Get access Rights & Permissions [Opens in a new window]

Extract

One might fairly say that the very meaning of our subject has changed since Hilbert introduced it under the name Beweistheorie (it was meant to be the principal tool for formulating Hubert's general conception of how to analyze mathematical reasoning). Specifically, the roles of the two principal elements of proof theory, namely the intuitive proofs accepted and the formal proofs (or derivations) studied, have turned out to be quite different from what Hilbert thought. In his view the hard work had been done in the discovery of formalization, and what remained was the study of certain given formal systems.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 33 , Issue 3 , 10 October 1968 , pp. 321 - 388
Copyright
Copyright © Association for Symbolic Logic 1968

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

[1]Bachmann, H., Die Normalfunktionen und das Problem der ausgezeichneten Folgen von Ordnungszahlen, Vierteljahrsschrift der naturforschenden Gesellschaft, vol. 95 (1950), pp. 115–147.Google Scholar
[2]Barwise, J., Thesis, Stanford University, Stanford, California, 1967.Google Scholar
[3]Craig, W., Satisfaction for nth order language defined in nth order, this Journal, vol. 30 (1965), pp. 13–21; Mathematical reviews, vol. 33 (1967), pp. 659–660, #3883.Google Scholar
[4]Crossley, J. N., Constructive order types. I, Formal systems and recursive functions, Amsterdam, 1964, pp. 189–264; reviewed in Zentralblatt.Google Scholar
[5]Feferman, S., Systems of predicative analysis, this Journal, vol. 29 (1964), pp. 1–30.Google Scholar
[6]Feferman, S., Systems of predicative analysis. II: Representation of ordinals, this Journal, vol. 33 (1968), June.Google Scholar
[7]Feferman, S. and Kreisel, G., Persistent and invariant formulas relative to theories of higher order, Bulletin of the American Mathematical Society, vol. 72 (1966), pp. 480–485.CrossRefGoogle Scholar
[8]Gentzen, G., Untersuchungen über das logische Schliessen, Mathematische Zeitschrift, vol. 39 (1934), pp. 176–210, pp. 405–431.CrossRefGoogle Scholar
[9]Gentzen, G., Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematische Annalen, vol. 112 (1936), pp. 493–565.CrossRefGoogle Scholar
[10]Gentzen, G., Neue Fassung des Widerspruchfreiheitsbeweises für die reine Zahlentheorie, Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, vol. 4 (1938), Hirzel, Leipzig.Google Scholar
[11]Gerber, H., On an extension of Schütte's Klammersymbols, Mathematische Annalen, vol. 174 (1967), pp. 202–216.CrossRefGoogle Scholar
[12]Gödel, K., Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, Dialectica, vol. 12 (1958), pp. 280–287.CrossRefGoogle Scholar
[13]Hanf, W., Incompactness in languages with infinitely long expressions, Fundamenta Mathematicae, vol. 53 (1964), pp. 309–324.CrossRefGoogle Scholar
[14]Hilbert, D., Grundlagen der Geometrie, 7th edition, Springer, Leipzig, Berlin, 1930.Google Scholar
[15]Hilbert, D. and Bernays, P., Grundlagen der Mathematik, vol. 2, Springer, Berlin, 1939.Google Scholar
[16]Howard, W. A., Bar induction, bar recursion, and the Σ11-axiom of choice, this Journal, vol. 28 (1963), p. 303.Google Scholar
[17]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
[18]Karp, C. R., Languages with expressions of infinite length, North-Holland, Amsterdam, 1964.Google Scholar
[19]Karp, C. R., Primitive recursive set functions: a formulation with applications to infinitary formal systems, this Journal, vol. 31 (1966), p. 294.Google Scholar
[20]Kleene, S. G., Introduction to metamathematics, Van Nostrana, Princeton, N.J., 1952.Google Scholar
[21]Kleene, S. C. and Vesley, R. E., Foundations of intuitionistic mathematics, North-Holland, Amsterdam, 1965; reviewed this Journal, vol. 31 (1966), pp. 258–261.Google Scholar
[22]Kreisel, G., Mathematical significance of consistency proofs, this Journal, vol. 23 (1958), pp. 155–182.Google Scholar
[23]Kreisel, G., Ordinal logics and the characterization of informal concepts of proof, International Congress of Mathematicians, Edinburgh, 1958, pp. 289–299.Google Scholar
[24]Kreisel, G., Interpretation of classical analysis by means of constructive functionals of finite type, Constructivity in mathematics, edited by Heyting, A., North-Holland, Amsterdam, 1959, pp. 101–128.Google Scholar
[25]Kreisel, G., Analysis of the Cantor-Bendixson theorem by means of the analytic hierarchy, Bulletin de l'Académie Polonaise des Sciences, vol. 7 (1959), pp. 621–626.Google Scholar
[26]Kreisel, G., La prédicativité, Bulletin de la Société Mathématique de France, vol. 88 (1960), pp. 371–391.CrossRefGoogle Scholar
[27]Kreisel, G., The status of the first ε-number in first-order arithmetic, this Journal, vol. 25 (1960), p. 390.Google Scholar
[28]Kreisel, G., Set theoretic problems suggested by the notion of potential totality, Proceedings of the symposium on infinitistic methods in the foundations of mathematics, Warsaw, Sept. 2–8, 1959 (1961), pp. 103–140.Google Scholar
[29]Kreisel, G., The axiom of choice and the class of hyperarithmetic functions, Dutch Academy A, vol. 65 (1962), pp. 307–319.Google Scholar
[30]Kreisel, G., Model-theoretic invariants; applications to recursive and hyperarithmetic operations, The theory of models, North-Holland, Amsterdam, 1965, pp. 190–205.Google Scholar
[31]Kreisel, G., Mathematical logic, Lectures on modern mathematics, vol. III, ed. Saaty, Wiley, N.Y., 1965, pp. 95–195.Google Scholar
[32]Kreisel, G., Mathematical logic: what has it done for the philosophy of mathematics?Bertrand Russell: Philosopher of the century, Allen and Unwin, London, 1967, pp. 201–272.Google Scholar
[33]Kreisel, G., Informal rigour and completeness proofs, Problems in the philosophy of mathematics, North-Holland, Amsterdam, 1967, pp. 138–171.CrossRefGoogle Scholar
[34]Kreisel, G., Relative recursiveness in metarecursion theory and relative recursive enumerability in metarecursion theory, this Journal, vol. 32 (1967), pp. 442–443.Google Scholar
[35]Kreisel, G. and Krivine, J. L., Elements of mathematical logic; theory of models, North-Holland, Amsterdam, 1967.Google Scholar
[36]Kreisel, G. and Levy, A., Reflection principles and their use for establishing the complexity of axiom systems, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, vol. 14 (1968) pp. 97–142.CrossRefGoogle Scholar
[37]Kreisel, G., Shoenfield, J. R., and Hao, Wang, Arithmetic concepts and recursive well orderings, Archiv für mathematische Logik und Grundlagenforschung, vol. 5 (1959), pp. 42–64.CrossRefGoogle Scholar
[38]Kripke, S., Transfinite recursions on admissible ordinals. I, II, this Journal, vol. 29 (1964), pp. 161–162.Google Scholar
[39]Kunen, K., Implicit definability and infinitary languages, this Journal, vol. 33 (1968), pp. 446–451.Google Scholar
[40]Levy, A., Definability in axiomatic set theory I, pp. 127–151 of Proc. 1964 Int. Congress for Logic, Methodology and Philosophy of Science, Amsterdam, 1964.Google Scholar
[41]Levy, A., A hierarchy of formulas in set theory, Memoirs of the American Mathematical Society, no. 57 (1965).Google Scholar
[42]Löb, M. H., Solution of a problem of Leon Henkin, this Journal, vol. 20 (1955), pp. 115–118.Google Scholar
[43]Löb, M. H., Cut elimination in type theory, this Journal, vol. 29 (1964), p. 220.Google Scholar
[44]Lorenz, K., Dialogspiele als semantische Grundlage von Logikkalkülen, Archiv für mathematische Logik und Grundlagenforschung (to appear).Google Scholar
[45]Lorenzen, P., Einführung in die operative Logik und Mathematik, Springer, Berlin, 1955.CrossRefGoogle Scholar
[46]Mostowski, A., On a generalization of quantifiers, Fundamenta mathematicae, vol. 44 (1957), pp. 12–36.CrossRefGoogle Scholar
[47]Mostowski, A., Representability of sets in formal systems, Recursive function theory, Proceedings of symposia in pure mathematics, vol. 5, American Mathematical Society, Providence, R.I., 1962, pp. 29–48.CrossRefGoogle Scholar
[48]Parikh, R. J., Some generalizations of the notion of well ordering, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, vol. 12 (1966), pp. 333–340, reviewed Mathematical Reviews, vol. 34 (1967), p. 758, #4131.CrossRefGoogle Scholar
[49]Robinson, A., Introduction to model theory and to the metamathematics of algebra, North-Holland, Amsterdam, 1963.Google Scholar
[50]Schütte, K., Beweistheorie, 1960, Springer, Berlin; reviewed this Journal, vol. 25 (1960), pp. 243–249.Google Scholar
[51]Schütte, K., Properties of simple type theory, this Journal, vol. 25 (1960), pp. 305–326.Google Scholar
[52]Schütte, K., Predicative well orderings, Formal systems and recursive functions, North-Holland, Amsterdam, 1965, pp. 279–302.Google Scholar
[53]Schütte, K., Recent results in proof theory, Internat. Congress of Mathematicians, Moscow, Aug., 1966, pp. 16–26.Google Scholar
[54]Scott, D. S., Logic with denumerably long formulas and finite strings of quantifiers, Theory of models, North-Holland, Amsterdam, 1965, pp. 329–341.Google Scholar
[55]Shepherdson, J. C., Non-standard models for fragments of number theory, The theory of models, North-Holland, Amsterdam, 1965, pp. 342–358.Google Scholar
[56]Shoenfield, J. R., On a restricted ω-rule, Bulletin de l'Académie Polonaise des Sciences, vol. 7 (1959), pp. 405–407.Google Scholar
[57]Solovay, R., A non-constructible Δ31-set of integers, Transactions of the American Mathematical Society, vol. 127 (1967), pp. 50–75.Google Scholar
[58]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. Proceedings of symposia pure mathematics, vol. 5, American Mathematical Society, Providence, R.I., 1962, pp. 1–27.CrossRefGoogle Scholar
[59]Tait, W. W., Functionals defined by transfinite recursion, this Journal, vol. 30 (1965), pp. 155–174.Google Scholar
[60]Tait, W. W., The substitution method, this Journal, vol. 30 (1965), pp. 175–192; reviewed Mathematical reviews, vol. 34 (1967), p. 201, #1162.Google Scholar
[61]Tait, W. W., Cut elimination in infinite prepositional logic, this Journal, vol. 31 (1966), pp. 151–152.Google Scholar
[62]Tait, W. W., A non-constructive proof of Gentzen's Hauptsatz for second order predicate logic, Bulletin of the American Mathematical Society, vol. 72 (1966), pp. 980–983.CrossRefGoogle Scholar
[63]Takeuti, G., On a generalized logical calculus, Japan journal of mathematics, vol. 23 (1953), pp. 39–96.Google Scholar
[64]Takeuti, G., Consistency proofs of subsystems of classical analysis, Annals of mathematics (2), vol. 86 (1967), pp. 299–348.CrossRefGoogle Scholar
[65]Tarski, A., Mostowski, A., and Robinson, R. M., Undecidable theories, North-Holland, Amsterdam, 1953.Google Scholar
[66]Vaught, R. L., Sentences true in all constructive models, this Journal, vol. 24 (1959), pp. 1–15.Google Scholar
[67]Ackermann, W., Die Widerspruchsfreiheit der allgemeinen Mengenlehre, Mathematische Annalen, vol. 114 (1937), pp. 305–315.CrossRefGoogle Scholar
[68]Ax, J., On ternary definite rational functions, Proceedings of the London Mathematical Society (to appear).Google Scholar
[69]Feferman, S., Arithmetization of metamathematics in a general setting, Fundamenta mathematicae, vol. 49 (1960), pp. 36–92.CrossRefGoogle Scholar
[70]Feferman, S., An ω-model for the hyperarithmetic comprehension axiom in which the Σ11-axiom of choice fails. International Congress of Mathematicians, Moscow, August 16–26, 1966.Google Scholar
[71]Feferman, S., Kreisel, G. and Orey, S., Faithful interpretations, Archiv für mathematische Logik und Grundlagenforschung, vol. 6 (1962), pp. 52–63.CrossRefGoogle Scholar
[72]Frajssé, R., Une notion de récursivité relative, pp. 323–328 in Infinitistic methods, Warsaw, (1961) Pergamon Press, New York; see also D. Lacombe, Deux généralisations de la notion de récursivité, Comptes rendus hebdomadaires des séances de l'académie des sciences, vol. 258 (1964), pp. 3141–3143 and pp. 3410–3413.Google Scholar
[73]Friedman, H., On subsystems of analysis, Notices of the American Mathematical Society, vol. 14 (1967), p. 144, 67T-54.Google Scholar
[74]Friedman, H., Thesis, Massachusetts Institute of Technology, 1967.Google Scholar
[75]Gandy, R., Relations between analysis and set theory, this Journal, vol. 32 (1967), p. 434.Google Scholar
[76]Gödel, K., Remarks before the Princeton Bicentennial Conference on problems in mathematics, pp. 84–88 in The undecidable, ed. Davis, M., Raven Press, New York, 1955.Google Scholar
[77]Henkin, L., Fragments of the prepositional calculus, this Journal, vol. 14 (1949), pp. 42–48.Google Scholar
[78]Hilbert, D., Neubegründung der Mathematik. Erste Mitteilung, Abhandlungen aus dem Mathematischen Seminar der Universität Hamburg, vol. 1 (1922), pp. 157–177.CrossRefGoogle Scholar
[79]Horn, A., The separation theorem of intuitionistic propositional calculus, this Journal, vol. 27 (1963), pp. 391–399, reviewed in Zentralblatt, vol. 117 (1965), p. 253.Google Scholar
[80]Keisler, H. J., First order properties of pairs of cardinals, Bulletin of the American Mathematical Society, vol. 72 (1966), pp. 141–144.CrossRefGoogle Scholar
[81]Kreisel, G., On the interpretation of nonfinitist proofs, this Journal, vol. 16 (1961), pp. 241–267.Google Scholar
[82]Kreisel, G., Note on arithmetic models for consistent formulae of the predicate calculus. II, Proceedings of the Eleventh International Congress of Philosophy (1953), pp. 39–49, Pergamon Press, New York.Google Scholar
[83]Kreisel, G., “Models, translations and interpretations,” pp. 25–50, in Mathematical interpretation of formal systems, Studies in logic and the foundations of mathematics, North-Holland, Amsterdam (1955).Google Scholar
[84]Kreisel, G., Relative consistency and translatability, this Journal, vol. 23 (1958), pp. 108–109.Google Scholar
[85]Kreisel, G., Relative consistency proofs, this Journal, vol. 23 (1958), pp. 109–110.Google Scholar
[86]Kreisel, G., On weak completeness of intuitionistic predicate logic, this Journal, vol. 27 (1962), pp. 139–158.Google Scholar
[87]Kreisel, G. and Wang, Hao, Some applications of formalized consistency proofs, Fundamenta mathematicae, vol. 42 (1955), pp. 101–110; and vol. 45 (1958), pp. 334–335.CrossRefGoogle Scholar
[88]Kripke, S. and Pour-El, M. B., Deduction-preserving recursive isomorphisms between theories, Bulletin of the American Mathematical Society, vol. 73 (1967), pp. 145–148; Also Fundamenta mathematicae, vol. 61 (1967), pp. 141–163.Google Scholar
[89]Lehman, R. S., Acta arithmetica, vol. 11 (1966), pp. 397–410.CrossRefGoogle Scholar
[90]Malitz, J. I., Thesis, University of California, Berkeley, 1966.Google Scholar
[91]Montague, R. M., Interpretability in terms of models, Indagationes, vol. 27 (1965), pp. 467–476.CrossRefGoogle Scholar
[92]Parsons, C., Reduction of inductions to quantifier-free induction, Notices of the American Mathematical Society, vol. 13 (1966), p. 740.Google Scholar
[93]Reznikoff, I., Thesis, University of Paris, also: Tout ensemble de formules de la logique classique est équivalent à un ensemble indépendent, Comptes rendus hebdomadaires des séances de l'academie des sciences, vol. 260 (1965), pp. 2385–2388.Google Scholar
[94]Rowbottom, F., Thesis, University of Wisconsin, Madison, 1964.Google Scholar
[95]Shepherdson, J. C., A non-standard model for a free variable fragment of number theory, Bulletin de l'Academie Polonaise des Sciences, vol. 12 (1964), pp. 79–86.Google Scholar
[96]Shoenfield, J. R., A relative consistency proof, this Journal, vol. 19 (1954), pp. 21–28.Google Scholar
[97]Shoenfield, J. R., The problem of predicativity, pp. 132–139 of: Essays on the foundations of mathematics, North-Holland, Amsterdam, 1962.Google Scholar
[98]Tait, W. W., Intensional interpretations of functionals of finite type. I, this Journal, vol. 32 (1967), pp. 198–212.Google Scholar
[99]Thomason, S. K., Forcing method and the upper semilattice of hyperdegrees, Transactions of the American Mathematical Society, vol. 129 (1967), pp. 38–57.CrossRefGoogle Scholar
[100]Vaught, R. L., The completeness theorem of logic with the added quantifier ‘there are uncountably many’, Fundamenta mathematicae, vol. 54 (1964), pp. 303–304.CrossRefGoogle Scholar
[101]Howard, W. A., Functional interpretation of bar induction by bar recursion, Compositio, vol. 20 (1968), pp. 107–124.Google Scholar