Skip to main content
SpringerLink
Log in

Meaning in Use

  • Chapter
  • First Online:
Dag Prawitz on Proofs and Meaning

Part of the book series: Outstanding Contributions to Logic ((OCTR,volume 7))

Abstract

The historical origins of provability semantics are illustrated by so far unexplored manuscript passages of Gentzen and Gödel. Next the determination of elimination rules in natural deduction through a generalized inversion principle is treated, proposed earlier by the authors as a pedagogical device. The notion of validity in intuitionistic logic is related to the notion of formal provability through a direct translation. Finally, it is shown how the correspondence between rules and meaning can be used for setting up complete labelled sequent calculi, first for intuitionistic logic with the remarkable property of invertibility of all the logical rules, and then for modal and related logics.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    We do not enter into the discussion of the background of this principle beyond Prawitz, but refer to Moriconi and Tesconi (2008) for that.

  2. 2.

    If that was his way, which is by no means certain as discussed in von Plato (2012).

References

  • Boretti, B., & Negri, S. (2009). Decidability for Priorean linear time using a fixed-point labelled calculus. In M. Giese & A. Waaler (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods (pp. 108–122). Berlin: Springer.

    Google Scholar 

  • Dyckhoff, R. (1988). Implementing a simple proof assistant. In Workshop on Programming for Logic Teaching: Proceedings 23/1988 (pp 49–59). University of Leeds: Centre for Theoretical Computer Science.

    Google Scholar 

  • Dyckhoff, R., & Negri, S. (2012). Proof analysis in intermediate logics. Archive for Mathematical Logic, 51(1–2), 71–92.

    Article  Google Scholar 

  • Garg, D., Genovese, V., & Negri, S. (2012). Countermodels from sequent calculi in multi-modal logics. In LICS 2012, IEEE computer society (pp. 315–324).

    Google Scholar 

  • Gentzen, G. (1934–1935). Untersuchungen Über das logische Schließen I. Mathematische Zeitschrift, 39(2), 176–210.

    Google Scholar 

  • Gentzen, G. (1936). The consistency of elementary number theory. In M. E. Szabo (Ed.), The Collected Papers of Gerhard Gentzen (pp. 132–213). Amsterdam: North-Holland Publishing Company.

    Google Scholar 

  • Hakli, R., & Negri, S. (2012). Does the deduction theorem fail for modal logic? Synthese, 187(3), 849–867.

    Article  Google Scholar 

  • Heyting, A. (1930). Die formalen Regeln der intuitionistischen Logik. In Sitzungsberichte der Preussischen Akademie der Wissenschaften (pp. 42–56)., Physikalisch- mathematische Klasse.

    Google Scholar 

  • Heyting, A. (1931). Die intuitionistische Grundlegung der Mathematik. Erkenntnis, 2(1), 106–115.

    Article  Google Scholar 

  • Hilbert, D., & Bernays, P. (1934). Grundlagen der Mathematik (Vol. 1). Berlin: Springer.

    Google Scholar 

  • Hodes, H. (1984). Axioms for actuality. Journal of Philosophical Logic, 13(1), 27–34.

    Article  Google Scholar 

  • Joachimski, F., & Matthes, R. (2003). Short proofs of normalization for the simply-typed \(\lambda \)-calculus, permutative conversions and Gödel’s T. Archive for Mathematical Logic, 42(1), 59–87.

    Article  Google Scholar 

  • Kaplan, D. (1966). Review of Kripke. The Journal of Symbolic Logic, 31(1), 120–122.

    Article  Google Scholar 

  • Kripke, S. A. (1963). Semantical analysis of modal logic I. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 9(5–6), 67–96.

    Google Scholar 

  • Lopez-Escobar, E. (1999). Standardizing the N systems of Gentzen. In X. Caicedo & C. Montenegro (Eds.), Models, Algebras, and Proofs (pp. 411–434). New York: Dekker.

    Google Scholar 

  • Martin-Löf, P. (1984). Intuistionistic Type Theory. Napoli: Bibliopolis.

    Google Scholar 

  • Moriconi, E., & Tesconi, L. (2008). On inversion principles. History and Philosophy of Logic, 29(2), 103–113.

    Article  Google Scholar 

  • Negri, S. (1999). Sequent calculus Proof Theory of intuitionistic apartness and order relations. Archive for Mathematical Logic, 38(8), 521–547.

    Article  Google Scholar 

  • Negri, S. (2003). Contraction-free sequent calculi for geometric theories, with an application to Barr’s theorem. Archive for Mathematical Logic, 42(4), 389–401.

    Article  Google Scholar 

  • Negri, S. (2005). Proof analysis in modal logic. Journal of Philosophical Logic, 34(5–6), 507–544.

    Article  Google Scholar 

  • Negri, S. (2009). Kripke completeness revisited. In G. Primiero & S. Rahman (Eds.), Acts of knowledge—History, Philosophy and Logic (pp. 247–282). London: College Publications.

    Google Scholar 

  • Negri, S., & von Plato, J. (1998). Cut elimination in the presence of axioms. The Bulletin of Symbolic Logic, 4(4), 418–435.

    Article  Google Scholar 

  • Negri, S., & von Plato, J. (2001). Structural Proof Theory. Cambridge: Cambridge UniversityPress.

    Google Scholar 

  • Negri, S., & von Plato, J. (2011). Proof Analysis: A contribution to Hilbert’s Last Problem. Cambridge: Cambridge University Press.

    Google Scholar 

  • von Plato, J. (2000). A problem of normal form in natural deduction. Mathematical Logic Quarterly, 46(1), 121–124.

    Article  Google Scholar 

  • von Plato, J. (2001). Natural deduction with general elimination rules. Archive for Mathematical Logic, 40(7), 541–567.

    Article  Google Scholar 

  • von Plato, J. (2006). Normal form and existence property for derivations in Heyting arithmetic. Acta Philosophica Fennica, 78, 159–163.

    Google Scholar 

  • von Plato, J. (2008). Gentzen’s proof of normalization for natural deduction. The Bulletin of Symbolic Logic, 14(2), 240–244.

    Article  Google Scholar 

  • von Plato, J. (2012). Gentzen’s proof systems: byproducts in a work of genius. The Bulletin of Symbolic Logic, 18(3), 313–367.

    Google Scholar 

  • Prawitz, D. (1965). Natural Deduction: Proof-theoretical Study. Stockholm: Almqvist & Wicksell.

    Google Scholar 

  • Prawitz, D. (1971). Ideas and results in Proof Theory. In J. E. Fenstad (Ed.), Proceedings of the Second Scandinavian Logic Symposium (pp. 235–307). Amsterdam: North-Holland Publishing Company.

    Chapter  Google Scholar 

  • Schroeder-Heister, P. (1984a). Generalized rules for quantifiers and the completeness of the intuitionistic operators & \(\vee \), \(\supset \), \(\curlywedge \), \(\forall \), \(\exists \). In M. Richter, et al. (Eds.), Computation and Proof Theory (Vol. 1104, pp. 399–426)., Lecture Notes in Mathematics Berlin: Springer.

    Google Scholar 

  • Schroeder-Heister, P. (1984b). A natural extension of natural deduction. The Journal of Symbolic Logic, 49(4), 1284–1300.

    Article  Google Scholar 

  • Simpson, A. (1994). Proof Theory and Semantics for Intuitionistic Modal Logic. PhD thesis, School of Informatics, University of Edinburgh.

    Google Scholar 

  • Tennant, N. (1992). Autologic. Edinburgh: Edinburgh University Press.

    Google Scholar 

  • Viganó, L. (2000). Labelled Non-classical Logics. Dordrecht: Kluwer Academic Publishers.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Philosophy, University of Helsinki, P.O.Box 24, 00014, Helsinki, Finland

    Sara Negri & Jan von Plato

Authors
  1. Sara Negri
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jan von Plato
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sara Negri .

Editor information

Editors and Affiliations

  1. Bochum, Germany

    Heinrich Wansing

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Negri, S., von Plato, J. (2015). Meaning in Use. In: Wansing, H. (eds) Dag Prawitz on Proofs and Meaning. Outstanding Contributions to Logic, vol 7. Springer, Cham. https://doi.org/10.1007/978-3-319-11041-7_10

Download citation

Publish with us

Policies and ethics

Search

Navigation