Skip to main content
SpringerLink
Log in

Existential instantiation and strong normalization

  • Conference paper
  • First Online:
Logical Foundations of Computer Science (LFCS 1997)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1234))

Included in the following conference series:

Abstract

We present a new manageable formulation of natural deduction with a rule of existential instantiation ∃xA[x]/A[b]. It simplifies skolemizing devices of earlier formulations, includes a new rule for disjunction and admits a proof of strong normalization. This opens way to the treatment of new systems for which only normal form theorems are known.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Gentzen G.: Untersuchungen über das logische Schliessen. Mathematische Zeitschrift, 39 (1934) 176–210, 405–431

    Google Scholar 

  2. Girard J.-Y., Lafont Y., Taylor P.: Proofs and Types, Cambridge University Press, Cambridge (1988)

    Google Scholar 

  3. Leivant D.: Existential instantiation in a system of natural deduction, Mathematish Centrum-ZW 13–73 (1973)

    Google Scholar 

  4. Mints G.: Lewis Systems and the System T. In Mints G.: Selected Papers in Proof Theory, North-Holland-Bibliopolis (1993), 221–294 (Russian Original 1974)

    Google Scholar 

  5. Mints G.: A Normal Form Theorem for Second-order Classical Logic with an Axiom of Choice, Math. USSR Izvestiya 32 N3 (1989) 587–605

    Google Scholar 

  6. Mints G.: Normal Deduction in the Intuitionistic Linear Logic, CSLI report, (1996)

    Google Scholar 

  7. Prawitz D.: Natural Deduction, Almquist and Wiksell (1965)

    Google Scholar 

  8. Prawitz D.: Ideas and Results in Proof Theory, In Proc. 2-nd Scand.Logic Symp., North-Holland, (1972) 235–308

    Google Scholar 

  9. Quine W.V.: On natural deduction, Journal of Symbolic Logic 15 (1950) 93–102

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Philosophy, Stanford University, 94305, Stanford, CA, USA

    G. Mints

Authors
  1. G. Mints
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Sergei Adian Anil Nerode

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mints, G. (1997). Existential instantiation and strong normalization. In: Adian, S., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 1997. Lecture Notes in Computer Science, vol 1234. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63045-7_26

Download citation

  • DOI: https://doi.org/10.1007/3-540-63045-7_26

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63045-6

  • Online ISBN: 978-3-540-69065-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation