Skip to main content
SpringerLink
Log in
Book cover

Natural Deduction, Hybrid Systems and Modal Logics pp 28–74Cite as

Standard Natural Deduction

  • Chapter
  • First Online:

Part of the book series: Trends in Logic ((TREN,volume 30))

Abstract

This Chapter is devoted to the description of standard systems of natural deduction (ND). After historical introduction in Section 2.1 we present some preliminary criteria which should be satisfied by any system of natural deduction. Sections 2.3 and 2.4 develop a systematization of existing systems based on two features: the kind of data used by a system and the format of proof setting. As a result we divide traditional ND systems into F- and S-systems (rules defined on formulae or sequents), and on L- and T-systems (linear or tree proofs). The division is not exhaustive as there may be systems operating on other types of items (e.g. labelled formulae – cf. Chapter 8) The main conclusion of this part is that almost all of the known variants of ND may be traced back to the independent works of Jaśkowski and Gentzen who started the investigation on non-axiomatic deductive systems.

This is a preview of subscription content, 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   189.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   249.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   249.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

Learn about institutional subscriptions

Notes

  1. 1.

    This is why we do not treat sequent calculi and tableau systems as examples of natural deduction systems. In ordinary SC we have only cumulative proofs and introduction rules, in tableau systems only indirect proofs and elimination rules.

  2. 2.

    Note that Jaśkowski did not use ⊥, so it is present in the formulation of rules as a metalinguistic sign of inconsistency. Also the names of rules are not original; he just used on the level of realization names like: rule I, rule II, ֵֵ. Note that in general we do not use the original names of rules from described systems since several authors either use different notation for the same things or the same names for different things.

  3. 3.

    In rules of elimination like \((\rightarrow E)\) we will ocassionaly use traditional distinction between major premise which contains eliminated constant, and minor premise.

  4. 4.

    Jaśkowski formulated also ND system for propositional logic with quantifiers.

  5. 5.

    In fact, Gentzen defined antecedents of sequents rather as lists of formulae, so he needs also a rule of permutation and contraction for elements of antecedents.

  6. 6.

    This is, for example, a solution of Dyckhoff in [81] with H denoting hypotheses (assumptions) and F denoting facts, i.e. assumptions and formulae inferred from them.

  7. 7.

    Similar way of description is in Wójcicki [285], where every deductive system consists of axioms, H-rules (i.e. sequents) and G-rules (i.e. sequent rules).

  8. 8.

    Cf. e.g. an algorithm in Chapter 4.

  9. 9.

    Additionally Jaśkowski has used a prefix S (from supposition) in front of any assumption.

  10. 10.

    It must be said that Jaśkowski was not as lucky as Gentzen, whose contribution into development of proof methods is widely known. There are a lot of books and papers using some variant of ND in Jaśkowski format but crediting it to Fitch or to Gentzen.

  11. 11.

    This remark applies to practically oriented ND; in systems constructed for the needs of theoretical investigation other solution may work better, e.g. von Plato/Negri idea of generalized elimination rules in [193] leading to smooth proof of normalization.

  12. 12.

    In Chapter 4 we will introduce some drastic modification of ND leading to “flat” (no additional subderivations) proofs.

  13. 13.

    For simplicity we keep the same names as for suitable rules in the calculus, but note that “rules” from the level of realization correspond only partially to them; cf. Section 2.5.4.

  14. 14.

    The version from [158] differs in even more respects; e.g. there are no boxes, no specified inference rules for connectives, no [RED].

  15. 15.

    One may notice that in some ND systems without explicit use of S-lines, their effect is simulated by some meta-system devices, e.g. in Pollock’s [218] or in Gabbay [99], where “almost” KM system is used.

  16. 16.

    There is no risk of confusion with the notion concerning formulae in sequents so, in this book, we will call them shortly parameters in accordance with the terminology of Fitting.

  17. 17.

    Actually, the problems was to state properly the restriction for ∀ introduction, in the presence of \((\exists E)\); a detailed account of it can be found in Pelletier [204] and in Fine [87].

  18. 18.

    Here and then we follow the convention of Section 2.5, where two instructions for assumption introduction were signed by (a) and (b).

  19. 19.

    But it may be the same since the depth is measured not by the number of boxes in general but by the maximal number of nested boxes, and the eliminated box may not be a member of this maximal sequence.

Reference

  1. Fitting, M. 1996. First-order logic and automated theorem proving. Berlin; Springer.

    Google Scholar 

  2. Rieger, L. 1967. Algebraic methods of mathematical logic. Prague: Academia.

    Google Scholar 

  3. Kalish, D., and R. Montague. 1957. Remarks on descriptions and natural deduction. Archiv. für Mathematische Logik und Grundlagen Forschung 3: 50–64, 65–73.

    Article  Google Scholar 

  4. Woleński, J. 1985. Filozoficzna szkoła Lwowsko-Warszawska. Warszawa: PWN.

    Google Scholar 

  5. Borkowski, L., and J. Słupecki. 1958. A logical system based on rules and its applications in teaching mathematical logic. Studia Logica 7: 71–113.

    Article  Google Scholar 

  6. Thomason, R. 1970. Symbolic logic. New York: Macmillan.

    Google Scholar 

  7. Gabbay, D. 1996. LDS-labelled deductive systems. Oxford: Clarendon Press.

    Google Scholar 

  8. Fitting, M. 1983. Proof methods for modal and intuitionistic logics. Dordrecht; Rei-del.

    Google Scholar 

  9. Indrzejczak, A. 1995. Dedukcja naturalna w logikach modalnych pierwszego rzȩdu. In Filozofia/Logika: Filozofia logiczna 1994, eds. J. Perzanowski, A. Pietruszczak, and C. Gorzka, 289–302, Wyd. Toruń: Uniwersytetu Mikołaja Kopernika.

    Google Scholar 

  10. Herbrand, J. 1930. Recherches sur la theorie de la demonstration. In Travaux de la Societe des Sciences et des Lettres de Varsovie, Classe III, Sciences Mathematiques et Physiques, Warsovie, 1930.

    Google Scholar 

  11. Łukasiewicz, J. 1951. Aristotle’s syllogistic from the standpoint of modern logic. Oxford: Clarendon Press.

    Google Scholar 

  12. Corcoran, J. 1972. Aristotle’s natural deduction system. In Ancient logic and its modern interpretations, ed. J. Corcoran. Dordrecht: Reidel.

    Google Scholar 

  13. Hertz, P. 1929. Über Axiomensysteme für Beliebige Satzsysteme. Mathematische Annalen 101: 457–514.

    Article  Google Scholar 

  14. Ben-Sasson, E., and A. Widgerson. 2001. Short proofs are narrow – resolution made simple. Journal of the ACM 48(2): 149–169.

    Article  Google Scholar 

  15. Suppes, P. 1957. Introduction to logic. Princeton: Van Nostrand.

    Google Scholar 

  16. Ebbinghaus, H.D., J. Flum, and W. Thomas. 1984. Mathematical logic. Berlin: Springer.

    Google Scholar 

  17. Feys, R., and J. Ladriere. 1955. Supplementary notes. In Recherches sur la deduction logique, french translation of Gentzen, Paris: Press Univ. de France.

    Google Scholar 

  18. Pelletier, F.J. 1998. Automated natural deduction in THINKER. Studia Logica 60: 3–43.

    Article  Google Scholar 

  19. Tarski, A. 1930. Fundamentale Begriffe der Methodologie der deduktiven Wissenschaften. Monatschefte für Mathematik und Physik, 37: 361–404.

    Article  Google Scholar 

  20. Gentzen, G. 1936. Die Widerspruchsfreiheit der Reinen Zahlentheorie. Mathematische Annalen 112: 493–565.

    Article  Google Scholar 

  21. Indrzejczak, A. 1998. Jaśkowski and Gentzen approaches to natural deduction and related systems. In The Lvov-Warsw school and contemporary philosophy, eds. K. Kijania-Placek and J.Woleński, 253–264, Dordrecht: Kluwer.

    Google Scholar 

  22. Suszko, R. 1948. W sprawie logiki bez aksjomatów. Kwartalnik Filozoficzny 17(3/4): 199–205.

    Google Scholar 

  23. Quine W. Van O. 1950. Methods of logic. New York: Colt.

    Google Scholar 

  24. Copi, I.M. 1954. Symbolic logic, New York: The Macmillan Company.

    Google Scholar 

  25. Fine, K. 1985. Reasoning with arbitrary objects. Oxford: Blackwell.

    Google Scholar 

  26. Krajicek, J. 1994. Lower bounds to the size of constant-depth propositional proofs. Journal of Symbolic Logic 59(1): 73–85.

    Article  Google Scholar 

  27. Dyckhoff, R. 1987. Implementing a simple proof assistant. In Proceedings of workshop on programming for logic teaching, eds. J. Derrick, and H.A. Lewis, 49–59.

    Google Scholar 

  28. Negri, S., and J. von Plato. 2001. Structural proof theory, Cambridge: Cambridge University Press.

    Google Scholar 

  29. Wójcicki, R. Theory of logical calculi. Dordrecht: Kluwer.

    Google Scholar 

  30. Prawitz, D. 1965. Natural deduction. Stockholm: Almqvist and Wiksell.

    Google Scholar 

  31. Lemmon, E.J. 1965. Beginning logic. London: Nelson.

    Google Scholar 

  32. Garson, J.W. 2006. Modal logic for philosophers. Cambridge: Cambridge University Press.

    Google Scholar 

  33. Kleene, S.C. 1952. Introduction to metamathematics. Amsterdam: North Holland.

    Google Scholar 

  34. Fitch, F. 1952. Symbolic logic. New York: Ronald Press Co.

    Google Scholar 

  35. Pelletier, F.J. 1999. A brief history of natural deduction. History and Philosophy of Logic 20: 1–31.

    Article  Google Scholar 

  36. Jaśkowski, S. 1929. Teoria dedukcji oparta na dyrektywach założeniowych. In Ksiȩ ga Pamiatkowa I Polskiego Zjazdu Matematycznego. Kraków: Uniwersytet Jagielloņski.

    Google Scholar 

  37. Herbrand, J. 1928. Abstract In Comptes Rendus des Seances de l’Academie des Sciences, vol. 186, 1275 Paris.

    Google Scholar 

  38. Gentzen, G. 1934. Untersuchungen über das Logische Schliessen. Mathematische Zeitschrift 39: 176–210, 405–431.

    Article  Google Scholar 

  39. Jaśkowski, S. 1934. On the rules of suppositions in formal logic. Studia Logica 1: 5–32.

    Google Scholar 

  40. Pollock, J.L. Logic: An introduction to the formal study of reasonong. Available on http://oscarhomme.socsci.arizona.edu/ftp/publications.html

  41. Hermes, H. 1963. Einführung in die Mathematische Logik. Stuttgart: Teubner.

    Google Scholar 

  42. Mates, B. 1953. Stoic logic. Berkeley: University of California Press.

    Google Scholar 

  43. Gentzen, G. 1932. Über die Existenz Unabhängiger Axiomensysteme zu Unendlichen Satzsystemen. Mathematische Annalen 107: 329–350.

    Article  Google Scholar 

  44. Barth, E.M., E.C. Krabbe. 1982. From Axiom to Dialogue. Berlin: Walter de Gruyter.

    Google Scholar 

  45. Bonevac, D. 1987. Deduction, Mountain View: Mayfield Press.

    Google Scholar 

  46. Kalish, D., and R. Montague. 1964. Logic, techniques of formal reasoning. New York: Harcourt, Brace and World.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. Logic, University of Lódz, Kopcinskiego 16/18, 90-232, Lódz, Poland

    Dr. Andrzej Indrzejczak

Authors
  1. Dr. Andrzej Indrzejczak
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Andrzej Indrzejczak .

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer Science+Business Media B.V.

About this chapter

Cite this chapter

Indrzejczak, A. (2010). Standard Natural Deduction. In: Natural Deduction, Hybrid Systems and Modal Logics. Trends in Logic, vol 30. Springer, Dordrecht. https://doi.org/10.1007/978-90-481-8785-0_2

Download citation

Publish with us

Policies and ethics

Search

Navigation