Top

Published in:

2010 | OriginalPaper | Chapter

2. Standard Natural Deduction

Author : Dr. Andrzej Indrzejczak

Published in: Natural Deduction, Hybrid Systems and Modal Logics

Publisher: Springer Netherlands

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Preliminaries

next chapter Other Deductive Systems

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.

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.

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

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

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.

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.

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).

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

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

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.

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.

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

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.

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

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.

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.

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].

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

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.

[95]

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

[234]

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

[158]

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.CrossRef

[283]

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

[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.CrossRef

[274]

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

[99]

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

[93]

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

[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.

[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.

[180]

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

[73]

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

[129]

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

[26]

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

[266]

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

[82]

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

[86]

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

[204]

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

[272]

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

[110]

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

[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.

[267]

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

[226]

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

[72]

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

[87]

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

[168]

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

[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.

[193]

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

[285]

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

[220]

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

[174]

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

[105]

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

[162]

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

[89]

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

[205]

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

[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.

[126]

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

[109]

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

[157]

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

[218]

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

[128]

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

[187]

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

[108]

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

[20]

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

[52]

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

[159]

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

Title: Standard Natural Deduction
Author: Dr. Andrzej Indrzejczak
Publisher: Springer Netherlands
Book: Natural Deduction, Hybrid Systems and Modal Logics
Print ISBN: 978-90-481-8784-3

Electronic ISBN: 978-90-481-8785-0

Copyright Year: 2010
DOI: https://doi.org/10.1007/978-90-481-8785-0_2

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner