Advertisement

An Extension of Gentzen’s Analysis of Logical Deduction to Second-Order Logic

  • O. F. Serebriannikov
Part of the Synthese Library book series (SYLI, volume 257)

Abstract

As far as this author knows, the existent proofs of the cut-elimination or normal form theorem make use of means that are not formalized in first-order arithmetic and in this sense cannot be considered elementary (cf. [2, 4, 5, 6]). The nonelementary proofs give rise to some kind of intellectual uneasiness because they take for granted (even if in a metalanguage) what should be proved.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    ]G. Gentzen. Untersuchungen über daslogische Schliessen. Mathematische Zeitschrift, 35, 1934.Google Scholar
  2. [2]
    J.-Y. Girard. Une extension de l’interprétation de Gödel à l’analyse et son application à l’éliminatin des coupures dans l’analyse et la théorie de types. In Proceedings of the second Scandinavian Logic Symposium, Amsterdam, London 1971.Google Scholar
  3. [3]
    D. Hilbert and P. Bernays. Grundlagen der Mathematik 1. Zweite Auflage, Berlin, 1968.Google Scholar
  4. [4]
    P. Matin-Löf. Hauptsatz for theory of species. In Proceedings of the second Scandinavian Logic Symposium, Amsterdam, London 1971.Google Scholar
  5. [5]
    D. Prawitz. Ideas and Results in proof theory. In Proceedings of the second Scandinavian Logic Symposium, Amsterdam, London 1971.Google Scholar
  6. [6]
    G. Takeuti. Proof Theory Amsterdam, 1975.Google Scholar
  7. [7]
    F. Serebriannikov. An elementary proof ofthe cut-elimination theorem in second orde logic. Issledovaniyapo neklassicheskim logikam. Moskow 1989. (In Russian.)Google Scholar

Copyright information

© Springer Science+Business Media Dordrecht 1996

Authors and Affiliations

  • O. F. Serebriannikov

There are no affiliations available

Personalised recommendations