Editing Natural deduction (section)

== History ==
Natural deduction grew out of a context of dissatisfaction with the axiomatizations of deductive reasoning common to the systems of [[David Hilbert|Hilbert]], [[Gottlob Frege|Frege]], and [[Bertrand Russell|Russell]] (see, e.g., [[Hilbert system]]). Such axiomatizations were most famously used by [[Bertrand Russell|Russell]] and [[Alfred North Whitehead|Whitehead]] in their mathematical treatise ''[[Principia Mathematica]]''. Spurred on by a series of seminars in Poland in 1926 by [[Jan Lukasiewicz|Łukasiewicz]] that advocated a more natural treatment of logic, [[Stanisław Jaśkowski|Jaśkowski]] made the earliest attempts at defining a more natural deduction, first in 1929 using a diagrammatic notation, and later updating his proposal in a sequence of papers in 1934 and 1935.{{sfn|Jaśkowski|1934}} His proposals led to different notations such as [[Fitch notation]] or [[Patrick Suppes|Suppes]]' method, for which [[John Lemmon|Lemmon]] gave a variant now known as [[Suppes–Lemmon notation]].

Natural deduction in its modern form was independently proposed by the German mathematician [[Gerhard Gentzen]] in 1933, in a dissertation delivered to the faculty of mathematical sciences of the [[University of Göttingen]].<ref>{{harvnb|Gentzen|1935a}}, {{harvnb|Gentzen|1935b}}.</ref> The term ''natural deduction'' (or rather, its German equivalent ''natürliches Schließen'') was coined in that paper:

{{verse translation|lang=de|Ich wollte nun zunächst einmal einen Formalismus aufstellen, der dem wirklichen Schließen möglichst nahe kommt. So ergab sich ein "Kalkül des natürlichen Schließens".{{sfn|Gentzen|1935a|p=176}}|First I wished to construct a formalism that comes as close as possible to actual reasoning. Thus arose a "calculus of natural deduction".}}

Gentzen was motivated by a desire to establish the consistency of [[number theory]]. He was unable to prove the main result required for the consistency result, the [[cut elimination theorem]]—the Hauptsatz—directly for natural deduction. For this reason he introduced his alternative system, the [[sequent calculus]], for which he proved the Hauptsatz both for [[Classical logic|classical]] and [[intuitionistic logic]]. In a series of seminars in 1961 and 1962 [[Dag Prawitz|Prawitz]] gave a comprehensive summary of natural deduction calculi, and transported much of Gentzen's work with sequent calculi into the natural deduction framework. His 1965 monograph ''Natural deduction: a proof-theoretical study''<ref name=prawitz1965>{{harvnb|Prawitz|1965}}, {{harvnb|Prawitz|2006}}.</ref> was to become a reference work on natural deduction, and included applications for [[modal logic|modal]] and [[second-order logic]].

In natural deduction, a [[proposition]] is deduced from a collection of premises by applying inference rules repeatedly. The system presented in this article is a minor variation of Gentzen's or Prawitz's formulation, but with a closer adherence to [[Per Martin-Löf|Martin-Löf]]'s description of logical judgments and connectives.{{sfn|Martin-Löf|1996}}

===History of notation styles===
Natural deduction has had a large variety of notation styles,{{sfn|Pelletier|Hazen|2024}} which can make it difficult to recognize a proof if you're not familiar with one of them. To help with this situation, this article has a {{section link||Notation}} section explaining how to read all the notation that it will actually use. This section just explains the historical evolution of notation styles, most of which cannot be shown because there are no illustrations available under a [[public copyright license]] – the reader is pointed to the [https://plato.stanford.edu/archives/spr2024/entries/natural-deduction/ SEP] and [https://iep.utm.edu/natural-deduction/ IEP] for pictures.
* [[Gerhard Gentzen|Gentzen]] invented natural deduction using tree-shaped proofs – see {{section link||Gentzen's tree notation}} for details.
* [[Stanisław Jaśkowski|Jaśkowski]] changed this to a notation that used various nested boxes.{{sfn|Pelletier|Hazen|2024}}
* [[Frederic Fitch|Fitch]] changed Jaśkowski method of drawing the boxes, creating [[Fitch notation]].{{sfn|Pelletier|Hazen|2024}}
* 1940: In a textbook, [[Willard Van Orman Quine|Quine]]<ref>{{harvtxt|Quine|1981}}. See particularly pages 91–93 for Quine's line-number notation for antecedent dependencies.</ref> indicated antecedent dependencies by line numbers in square brackets, anticipating Suppes' 1957 line-number notation.
* 1950: In a textbook, {{harvtxt|Quine|1982|pp=241–255}} demonstrated a method of using one or more asterisks to the left of each line of proof to indicate dependencies. This is equivalent to Kleene's vertical bars. (It is not totally clear if Quine's asterisk notation appeared in the original 1950 edition or was added in a later edition.)
* 1957: An introduction to practical logic theorem proving in a textbook by {{harvtxt|Suppes|1999|pp=25–150}}. This indicated dependencies (i.e. antecedent propositions) by line numbers at the left of each line.
* 1963: {{harvtxt|Stoll|1979|pp=183–190, 215–219}} uses sets of line numbers to indicate antecedent dependencies of the lines of sequential logical arguments based on natural deduction inference rules.
* 1965: The entire textbook by {{harvtxt|Lemmon|1978}} is an introduction to logic proofs using a method based on that of [[Patrick Suppes|Suppes]], what is now known as [[Suppes–Lemmon notation]].
* 1967: In a textbook, {{harvtxt|Kleene|2002|pp=50–58, 128–130}} briefly demonstrated two kinds of practical logic proofs, one system using explicit quotations of antecedent propositions on the left of each line, the other system using vertical bar-lines on the left to indicate dependencies.{{refn|A particular advantage of Kleene's tabular natural deduction systems is that he proves the validity of the inference rules for both propositional calculus and predicate calculus. See {{harvnb|Kleene|2002|pp=44–45, 118–119}}.}}