Standard Natural Deduction

  • Andrzej IndrzejczakEmail author
Part of the Trends in Logic book series (TREN, volume 30)


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.


Inference Rule Deductive System Axiom System Natural Deduction Sequent Calculus 
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.


  1. [95]
    Fitting, M. 1996. First-order logic and automated theorem proving. Berlin; Springer.Google Scholar
  2. [234]
    Rieger, L. 1967. Algebraic methods of mathematical logic. Prague: Academia.Google Scholar
  3. [158]
    Kalish, D., and R. Montague. 1957. Remarks on descriptions and natural deduction. Archiv. r Mathematische Logik und Grundlagen Forschung 3: 50–64, 65–73.CrossRefGoogle Scholar
  4. [283]
    Woleński, J. 1985. Filozoficzna szkoła Lwowsko-Warszawska. Warszawa: PWN.Google Scholar
  5. [54]
    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.CrossRefGoogle Scholar
  6. [274]
    Thomason, R. 1970. Symbolic logic. New York: Macmillan.Google Scholar
  7. [99]
    Gabbay, D. 1996. LDS-labelled deductive systems. Oxford: Clarendon Press.Google Scholar
  8. [93]
    Fitting, M. 1983. Proof methods for modal and intuitionistic logics. Dordrecht; Rei-del.Google Scholar
  9. [141]
    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. [127]
    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. [180]
    Łukasiewicz, J. 1951. Aristotle’s syllogistic from the standpoint of modern logic. Oxford: Clarendon Press.Google Scholar
  12. [73]
    Corcoran, J. 1972. Aristotle’s natural deduction system. In Ancient logic and its modern interpretations, ed. J. Corcoran. Dordrecht: Reidel.Google Scholar
  13. [129]
    Hertz, P. 1929. Über Axiomensysteme für Beliebige Satzsysteme. Mathematische Annalen 101: 457–514.CrossRefGoogle Scholar
  14. [26]
    Ben-Sasson, E., and A. Widgerson. 2001. Short proofs are narrow – resolution made simple. Journal of the ACM 48(2): 149–169.CrossRefGoogle Scholar
  15. [266]
    Suppes, P. 1957. Introduction to logic. Princeton: Van Nostrand.Google Scholar
  16. [82]
    Ebbinghaus, H.D., J. Flum, and W. Thomas. 1984. Mathematical logic. Berlin: Springer.Google Scholar
  17. [86]
    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. [204]
    Pelletier, F.J. 1998. Automated natural deduction in THINKER. Studia Logica 60: 3–43.CrossRefGoogle Scholar
  19. [272]
    Tarski, A. 1930. Fundamentale Begriffe der Methodologie der deduktiven Wissenschaften. Monatschefte r Mathematik und Physik, 37: 361–404.CrossRefGoogle Scholar
  20. [110]
    Gentzen, G. 1936. Die Widerspruchsfreiheit der Reinen Zahlentheorie. Mathematische Annalen 112: 493–565.CrossRefGoogle Scholar
  21. [144]
    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. [267]
    Suszko, R. 1948. W sprawie logiki bez aksjomatów. Kwartalnik Filozoficzny 17(3/4): 199–205.Google Scholar
  23. [226]
    Quine W. Van O. 1950. Methods of logic. New York: Colt.Google Scholar
  24. [72]
    Copi, I.M. 1954. Symbolic logic, New York: The Macmillan Company.Google Scholar
  25. [87]
    Fine, K. 1985. Reasoning with arbitrary objects. Oxford: Blackwell.Google Scholar
  26. [168]
    Krajicek, J. 1994. Lower bounds to the size of constant-depth propositional proofs. Journal of Symbolic Logic 59(1): 73–85.CrossRefGoogle Scholar
  27. [81]
    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. [193]
    Negri, S., and J. von Plato. 2001. Structural proof theory, Cambridge: Cambridge University Press.Google Scholar
  29. [285]
    Wójcicki, R. Theory of logical calculi. Dordrecht: Kluwer.Google Scholar
  30. [220]
    Prawitz, D. 1965. Natural deduction. Stockholm: Almqvist and Wiksell.Google Scholar
  31. [174]
    Lemmon, E.J. 1965. Beginning logic. London: Nelson.Google Scholar
  32. [105]
    Garson, J.W. 2006. Modal logic for philosophers. Cambridge: Cambridge University Press.Google Scholar
  33. [162]
    Kleene, S.C. 1952. Introduction to metamathematics. Amsterdam: North Holland.Google Scholar
  34. [89]
    Fitch, F. 1952. Symbolic logic. New York: Ronald Press Co.Google Scholar
  35. [205]
    Pelletier, F.J. 1999. A brief history of natural deduction. History and Philosophy of Logic 20: 1–31.CrossRefGoogle Scholar
  36. [156]
    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. [126]
    Herbrand, J. 1928. Abstract In Comptes Rendus des Seances de l’Academie des Sciences, vol. 186, 1275 Paris.Google Scholar
  38. [109]
    Gentzen, G. 1934. Untersuchungen über das Logische Schliessen. Mathematische Zeitschrift 39: 176–210, 405–431.CrossRefGoogle Scholar
  39. [157]
    Jaśkowski, S. 1934. On the rules of suppositions in formal logic. Studia Logica 1: 5–32.Google Scholar
  40. [218]
    Pollock, J.L. Logic: An introduction to the formal study of reasonong. Available on
  41. [128]
    Hermes, H. 1963. Einführung in die Mathematische Logik. Stuttgart: Teubner.Google Scholar
  42. [187]
    Mates, B. 1953. Stoic logic. Berkeley: University of California Press.Google Scholar
  43. [108]
    Gentzen, G. 1932. Über die Existenz Unabhängiger Axiomensysteme zu Unendlichen Satzsystemen. Mathematische Annalen 107: 329–350.CrossRefGoogle Scholar
  44. [20]
    Barth, E.M., E.C. Krabbe. 1982. From Axiom to Dialogue. Berlin: Walter de Gruyter.Google Scholar
  45. [52]
    Bonevac, D. 1987. Deduction, Mountain View: Mayfield Press.Google Scholar
  46. [159]
    Kalish, D., and R. Montague. 1964. Logic, techniques of formal reasoning. New York: Harcourt, Brace and World.Google Scholar

Copyright information

© Springer Science+Business Media B.V. 2010

Authors and Affiliations

  1. 1.Dept. LogicUniversity of LódzLódzPoland

Personalised recommendations