Lectures on proof theory

  • Solomon Feferman
Conference paper
Part of the Lecture Notes in Mathematics book series (LNM, volume 70)


Inductive Hypothesis Atomic Formula Proof Theory Relation Symbol Interpolation Theorem 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Ba]
    Bachmann, H., Transfinite Zahlen, Springer, Berlin (1955)CrossRefzbMATHGoogle Scholar
  2. [Bw]
    Barwise, K. J., Infinitary logic and admissible sets, Dissertation, Stanford University (1967).Google Scholar
  3. [Be]
    Beth, E. W., On Padoa's method in the theory of definition Indag. Math., v. 15 (1953), pp. 330–339.MathSciNetCrossRefzbMATHGoogle Scholar
  4. [Ch]
    Choodnovsky, G., Some results in theory of infinitely long expressions, (abstract) Proc. 3d Intl. Cong. for Logic, Methodology and Philos. of Science, Amsterdam, 1967 (to appear).Google Scholar
  5. [Crl]
    Craig, W., Linear reasoning. A new form of the Herbrand-Gentzen theorem, Journ. Symbolic Logic, v. 22 (1957), pp. 250–268.MathSciNetCrossRefzbMATHGoogle Scholar
  6. [Cr2]
    -, Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory, Journ. Symbolic Logic, v. 22 (1957), pp. 269–285.MathSciNetCrossRefzbMATHGoogle Scholar
  7. [Ff1]
    Feferman, S., Systems of predicative analysis, Journ. Symbolic Logic, v. 29 (1964) pp. 1–30.MathSciNetCrossRefzbMATHGoogle Scholar
  8. [Ff2]
    Feferman, S., Systems of predicative analysis, II: representations of ordinals, Journ. Symbolic Logic (to appear).Google Scholar
  9. [Ff3]
    Feferman, S., Autonomous transfinite progressions and the extent of predicative mathematics, Proc. 3d Intl. Cong. for Logic, Methodology and Philos. of Science, Amsterdam, 1967 (to appear).Google Scholar
  10. [Ff4]
    Feferman, S., Persistent and invariant formulas for outer extensions, Compos. Math. (to appear).Google Scholar
  11. [F, K]
    Feferman, S. and G. Kreisel, Persistent and invariant formulas relative to theories of higher order, (Research Announcement) Bull. Amer. Math. Soc. v. 72 (1966), pp. 480–485.MathSciNetCrossRefzbMATHGoogle Scholar
  12. [Fr]
    Fraïssé, R., Une notion de récursivité relative, in Infinitistic Methods (Proc. Symp. founds. maths, Warsaw, 1959) Pergamon, Oxford (1961), pp. 323–328.Google Scholar
  13. [Gn1]
    Gentzen, G., Untarsuchungen über das logische Schlaessen, Math. Zeitschr. v. 39 (1934) pp. 176–210, 405–431.MathSciNetCrossRefzbMATHGoogle Scholar
  14. [Gn2]
    -, Die Widerspruchsfreiheit der reinen Zahlentheorie, Math. Annalen, v. 112 (1936), pp. 493–565.MathSciNetCrossRefzbMATHGoogle Scholar
  15. [Gn3]
    -, Neue Fassung des Widerspruchsfreiheitsbeweis fur die reine Zahlentheorie, Forsch. zur Logik und zur Grundlegung der exacten Wissenschaften, no. 4 (1938), Leipzig pp. 19–44.zbMATHGoogle Scholar
  16. [Gn4]
    -, Beweisbarkeit und Unbeweisbarkeit von Anfangsfallen der transfiniten Induktion in der reinen Zahlentheorie, Math. Annalen, v. 119 (1943) pp. 140–161.MathSciNetCrossRefzbMATHGoogle Scholar
  17. [Gdl-]
    Gödel, K., Über formal unentscheidbare Satze der Principia Mathematica und verwandter Systeme I. Monats. Math., Physik v. 38 (1931) pp. 173–198 (transl. in [vH], pp. 596–616).CrossRefzbMATHGoogle Scholar
  18. [Gd2]
    -, Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, Dialectica, v. 12 (1958), pp. 280–287.MathSciNetCrossRefzbMATHGoogle Scholar
  19. [G,M,R]
    Grzegorczyk, A., A. Mostowski and C. Ryll-Nardzewski, The classical and the ω-complete arithmetic, Journ. Symbolic Logic, v. 23 (1958), pp. 188–206.MathSciNetCrossRefzbMATHGoogle Scholar
  20. [vH]
    van Heijenoort, J. (ed.) From Frege to Gödel (A source book in mathematical logic, 1879–1931), Harvard Univ. Press, Cambridge (1967).zbMATHGoogle Scholar
  21. [Hn]
    Henkin, L., An extension of the Craig-Lyndon interpolation theorem, Journ. Symbolic Logic, v. 28 (1963), pp. 201–216.MathSciNetCrossRefzbMATHGoogle Scholar
  22. [Hr]
    Herbrand, J. Recherches sur la théorie de la demonstration. Trav. Soc. Sciences, Lettres de Varsovie, Cl. III no. 33 (1930), 128 pp. (transl. in part in [vH], pp. 525–581).Google Scholar
  23. [Hl]
    Hilbert, D. Über das unendlichen, Math. Annalen, v. 95 (1926), pp. 161–190 (transl. in [vH], pp. 367–392).MathSciNetCrossRefGoogle Scholar
  24. [H,B]
    Hilbert, D. and P. Bernays, Grundlagen der Mathematik, vol. 2, Springer, Berlin (1939).zbMATHGoogle Scholar
  25. [Kp]
    Karp, C., Languages with expressions of infinite length, North-Holland, Amsterdam (1964).zbMATHGoogle Scholar
  26. [Ks1]
    Keisler, H. J., Theory of models with generalized atomic formulas, Journ. Symbolic Logic, v. 25 (1960), pp. 1–26.MathSciNetCrossRefzbMATHGoogle Scholar
  27. [Ks2]
    -, Ultraproducts and elementary classes, Indag. Math., v. 23 (1961), pp. 477–495.MathSciNetCrossRefzbMATHGoogle Scholar
  28. [Ks3]
    -, Some applications of infinitely long formulas, Journ. Symbolic Logic, v. 30 (1965), pp. 339–349.MathSciNetCrossRefzbMATHGoogle Scholar
  29. [Kl]
    Kleene, S. C. Introduction to metamathematics, Van Nostrand, Princeton (1952).zbMATHGoogle Scholar
  30. [Ko1]
    Kochen, S., Completeness of algebraic systems in higher order calculi, in Summaries of talks presented at the summer institute for symbolic logic, Cornell University 1957, 2nd edition, Inst. for Def. Analyses (1960), pp. 370–376.Google Scholar
  31. [Ko2]
    -, Ultraproducts in the theory of models, Annals Math., v. 74 (1961) pp. 231–261.MathSciNetCrossRefzbMATHGoogle Scholar
  32. [Kr1]
    Kreisel, G., Model-theoretic invariants: applications to recursive and hyperarithmetic operations, in The theory of models (eds. Addison, Henkin, Tarski), North-Holland, Amsterdam (1965), pp. 190–205.Google Scholar
  33. [Kr2]
    -, Relative recursiveness in metarecursion theory (abstract) Journ. Symbolic Logic, v. 33 (1969), p. 442.MathSciNetGoogle Scholar
  34. [Kr3]
    Kreisel, G., A survey of proof theory, Journ. Symbolic Logic (to appear).Google Scholar
  35. [Kr4]
    Kreisel, G., So-called consistency proofs by means of transfinite induction (provable ordinals) (abstract for Leeds meeting ASL, 1967), Journ. Symbolic Logic (to appear).Google Scholar
  36. [K, K]
    Kreisel, G. and J. L. Krivine, Elements of mathematical logic (model theory), North-Holland, Amsterdam (1967).zbMATHGoogle Scholar
  37. [K, S]
    Kreisel, G. and G. Sacks, Metarecursion theory, Journ. Symbolic Logic, v. 30 pp. 318–338.Google Scholar
  38. [Kk]
    Kripke, S., Transfinite recursion on admissible ordinals, I, II, (abstracts) Journ. Symbolic Logic v. 29 (1964), pp. 161–162.Google Scholar
  39. [Ku]
    Kunen, K., Implicit definability and infinitary languages, Journ. Symbolic Logic (to appear).Google Scholar
  40. [Lv]
    Lévy, A., A hierarchy of formulas in set theory, Memoirs Amer. Math. Soc., no. 57 (1965).Google Scholar
  41. [L-E1]
    Lopez-Escobar, E. G. K., An interpolation theorem for denumerably long formulas, Fund. Math. v. 57 (1965), pp. 253–272.MathSciNetzbMATHGoogle Scholar
  42. [L-E2]
    -, Remarks on an infinitary language with constructive formulas, Journ. Symbolic Logic v. 32 (1967), pp. 305–318.MathSciNetCrossRefzbMATHGoogle Scholar
  43. [Lr]
    Lorenzen, P., Algebraische und logistische Untersuchungen über freie Verbände, Journ. Symbolic Logic, v. 16 (1951) pp. 81–106.MathSciNetCrossRefzbMATHGoogle Scholar
  44. [Ls]
    Łos, J., On the extending of models, I, Fund. Math. v. 42 (1955), pp. 38–54.MathSciNetzbMATHGoogle Scholar
  45. [Lyl]
    Lyndon, R., An interpolation theorem in the predicate calculus, Pacif. Journ. Math., v. 9 (1959), pp. 129–142.MathSciNetCrossRefzbMATHGoogle Scholar
  46. [Ly2]
    -, Properties preserved under homomorphism, Pacif. Journ. Math. v. 9 (1959), pp. 253–272.MathSciNetzbMATHGoogle Scholar
  47. [Mh]
    Maehara, S., On the interpolation theorem of Craig (Japanese), Sûgaku v. 12 (1960/61), pp. 235–237.MathSciNetzbMATHGoogle Scholar
  48. [Mk]
    Makkai, M., Preservation theorems for the logic with denumerable conjunctions and disjunctions, to appear in Journal Symbolic Logic.Google Scholar
  49. [Ml]
    Malitz, J. I., Problems in the model theory of infinite languages, Dissertation, University of California at Berkeley (1965).Google Scholar
  50. [Mn]
    Mendelson, E., Introduction to mathematical logic, Van Nostrand, Princeton (1964).zbMATHGoogle Scholar
  51. [N]
    Novikov, P. S., Inconsistencies of certain logical calculi (Russian) in Infinitistic methods (Proc. symp. founds. maths., Warsaw, 1959), Pergamon, Oxford, 1961, pp. 71–74.Google Scholar
  52. [O]
    Oberschelp, A., Untersuchungen zur mehrsortigen Quantorenlogik, Math. Annalen, v. 145 (1962), pp. 297–333.MathSciNetCrossRefzbMATHGoogle Scholar
  53. [Pl]
    Platek, R., Foundations of recursion theory, Dissertation, Stanford University (1966).Google Scholar
  54. [Pr]
    Prawitz, D., Naturaldeduction. A proof theoretical study. Acta Univ. Stock., Stockholm studies in philosophy, no. 3 (1965).Google Scholar
  55. [R]
    Robinson, A., Introduction to model theory and to the metamathematics of algebra, North-Holland, Amsterdam (1963).zbMATHGoogle Scholar
  56. [Sch1]
    Schütte, K., Beweistheorie, Springer, Berlin (1960).zbMATHGoogle Scholar
  57. [Sch2]
    -, Predicative well-orderings, in Formal systems and recursive functions (eds. Crossley, Dummett), North-Holland, Amsterdam (1963), pp. 279–302.Google Scholar
  58. [Sch3]
    -, Eine grenze fur die Beweisbarkeit der Transfiniten Induktion in der verzweigten Typenlogik, Arch. math. Logik, Grundl., v. 7 (1965) pp. 45–60.MathSciNetCrossRefzbMATHGoogle Scholar
  59. [Sch4]
    -, Der Interpolationssatz der intuitionistischen Prädikatenlogik, Math. Annalen, v. 148 (1962), pp. 192–200.CrossRefzbMATHGoogle Scholar
  60. [Scl]
    Scott, D., Logic with denumerable long formulas and finite strings of quantifiers, in The theory of models (eds. Addison, Henkin, Tarski), North-Holland, Amsterdam (1965), pp. 32–341.Google Scholar
  61. [Sc2]
    Scott, D., Interpolation theorems, Proc. 3d Intl. Cong. for Logic, Methodology and Philos. of Science, Amsterdam 1967 (to appear).Google Scholar
  62. [S,T]
    Scott, D. and A. Tarski, Extension principles for algebrakolly closed fields, (abstract) Notices Amer. Math. Soc., v. 5 (1958), pp. 778–779.Google Scholar
  63. [Sh]
    Shoenfield, J. R., Mathematical Logic, Addison-Wesley, Reading (1967).zbMATHGoogle Scholar
  64. [Sm]
    Smullyan, R. M., A unifying principle in quantification theory, in The theory of models (eds. Addison, Henkin, Tarski), North-Holland, Amsterdam, 1965, pp. 433–434.Google Scholar
  65. [Tt]
    Tait, W. W., Normal derivability in classical logic, Journ. Symbolic Logic (to appear).Google Scholar
  66. [Tk1]
    Takeuti, G., Consistency proofs of subsystems of classical analysis, Annals Math., v. 86 (1967), pp. 299–348.MathSciNetCrossRefzbMATHGoogle Scholar
  67. [Tk2]
    Takeuti, G., Π 11-comprehension axioms and ω-rule, Proc. Leeds 1967 Inst. in Logic (this volume).Google Scholar
  68. [Tr]
    Tarski, A. Contributions to the theory of models, Indag. Math. v. 16 (1954), Part I pp. 572–581, Part II pp. 582–588.MathSciNetCrossRefzbMATHGoogle Scholar
  69. [T,V]
    Tarski, A. and R. L. Vaught, Arithmetical extensions of relational systems, Compos. Math. v. 13 (1957), pp. 81–102.MathSciNetzbMATHGoogle Scholar
  70. [V]
    Vaught, R. L., Applications of the Löwenheim-Skolem-Tarski theorem to problems of completeness and decidability. Indag. Math., v. 16 (1954), pp. 467–472.MathSciNetCrossRefzbMATHGoogle Scholar
  71. [Wg]
    Wang, H., Logic of many sorted theories, Journ. Symbolic Logic, v. 17 (1952), pp. 105–116.MathSciNetCrossRefzbMATHGoogle Scholar
  72. [Wl]
    Weil, A., Foundations of algebraic geometry, Amer. Math. Soc. Colloq. Publs. v. 29, Rev. Ed. (1962).Google Scholar
  73. [Kp2]
    Karp, C., Finite-quantifier equivalence in The theory of models (eds. Addison, Henkin, Tarski), North-Holland, Amsterdam, 1965, pp. 407–412.Google Scholar

Copyright information

© Springer-Verlag 1968

Authors and Affiliations

  • Solomon Feferman

There are no affiliations available

Personalised recommendations