Natural deduction

In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the 'natural' way of reasoning. This contrasts with Hilbert-style systems, which instead use axioms as much as possible to express the logical laws of deductive reasoning.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'. A  true B  true ( A ∧ B )  true   ∧ I {displaystyle {frac {A{hbox{ true}}qquad B{hbox{ true}}}{(Awedge B){hbox{ true}}}} wedge _{I}} A  prop B  prop A  true B  true ( A ∧ B )  true   ∧ I {displaystyle {frac {A{hbox{ prop}}qquad B{hbox{ prop}}qquad A{hbox{ true}}qquad B{hbox{ true}}}{(Awedge B){hbox{ true}}}} wedge _{I}} A ∧ B  prop A  true B  true ( A ∧ B )  true   ∧ I {displaystyle {frac {Awedge B{hbox{ prop}}qquad A{hbox{ true}}qquad B{hbox{ true}}}{(Awedge B){hbox{ true}}}} wedge _{I}}   ⊤  true   ⊤ I {displaystyle {frac { }{ op {hbox{ true}}}} op _{I}} A  true A ∨ B  true   ∨ I 1 B  true A ∨ B  true   ∨ I 2 {displaystyle {frac {A{hbox{ true}}}{Avee B{hbox{ true}}}} vee _{I1}qquad {frac {B{hbox{ true}}}{Avee B{hbox{ true}}}} vee _{I2}} A ∧ B  true A  true   ∧ E 1 A ∧ B  true B  true   ∧ E 2 {displaystyle {frac {Awedge B{hbox{ true}}}{A{hbox{ true}}}} wedge _{E1}qquad {frac {Awedge B{hbox{ true}}}{B{hbox{ true}}}} wedge _{E2}} A ∧ B  true B  true   ∧ E 2 A ∧ B  true A  true   ∧ E 1 B ∧ A  true   ∧ I {displaystyle {cfrac {{cfrac {Awedge B{hbox{ true}}}{B{hbox{ true}}}} wedge _{E2}qquad {cfrac {Awedge B{hbox{ true}}}{A{hbox{ true}}}} wedge _{E1}}{Bwedge A{hbox{ true}}}} wedge _{I}} A ∧ ( B ∧ C )  true B ∧ C  true B  true   ∧ E 1   ∧ E 2 {displaystyle {cfrac {Awedge left(Bwedge C ight){hbox{ true}}}{{cfrac {Bwedge C{hbox{ true}}}{B{hbox{ true}}}} wedge _{E1}}} wedge _{E2}} A ∧ ( B ∧ C )  true ⋮ B  true {displaystyle {egin{matrix}Awedge left(Bwedge C ight){hbox{ true}}\vdots \B{hbox{ true}}end{matrix}}} D 1 D 2   ⋯   D n ⋮ J {displaystyle {egin{matrix}D_{1}quad D_{2} cdots D_{n}\vdots \Jend{matrix}}} A  true   u ⋮ B  true A ⊃ B  true   ⊃ I u A ⊃ B  true A  true B  true   ⊃ E {displaystyle {cfrac {egin{matrix}{cfrac {}{A{hbox{ true}}}} u\vdots \B{hbox{ true}}end{matrix}}{Asupset B{hbox{ true}}}} supset _{I^{u}}qquad {cfrac {Asupset B{hbox{ true}}quad A{hbox{ true}}}{B{hbox{ true}}}} supset _{E}} A  true   u B  true   w A ∧ B  true   ∧ I B ⊃ ( A ∧ B )  true A ⊃ ( B ⊃ ( A ∧ B ) )  true   ⊃ I u   ⊃ I w {displaystyle {cfrac {{cfrac {{cfrac {}{A{hbox{ true}}}} uquad {cfrac {}{B{hbox{ true}}}} w}{Awedge B{hbox{ true}}}} wedge _{I}}{{cfrac {Bsupset left(Awedge B ight){hbox{ true}}}{Asupset left(Bsupset left(Awedge B ight) ight){hbox{ true}}}} supset _{I^{u}}}} supset _{I^{w}}} A ∨ B  true A  true   u ⋮ C  true B  true   w ⋮ C  true C  true   ∨ E u , w {displaystyle {cfrac {Avee B{hbox{ true}}quad {egin{matrix}{cfrac {}{A{hbox{ true}}}} u\vdots \C{hbox{ true}}end{matrix}}quad {egin{matrix}{cfrac {}{B{hbox{ true}}}} w\vdots \C{hbox{ true}}end{matrix}}}{C{hbox{ true}}}} vee _{E^{u,w}}} ⊥  true C  true   ⊥ E {displaystyle {frac {perp {hbox{ true}}}{C{hbox{ true}}}} perp _{E}} A  true   u ⋮ p  true ¬ A  true   ¬ I u , p ¬ A  true A  true C  true   ¬ E {displaystyle {cfrac {egin{matrix}{cfrac {}{A{hbox{ true}}}} u\vdots \p{hbox{ true}}end{matrix}}{lnot A{hbox{ true}}}} lnot _{I^{u,p}}qquad {cfrac {lnot A{hbox{ true}}quad A{hbox{ true}}}{C{hbox{ true}}}} lnot _{E}} In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the 'natural' way of reasoning. This contrasts with Hilbert-style systems, which instead use axioms as much as possible to express the logical laws of deductive reasoning. Natural deduction grew out of a context of dissatisfaction with the axiomatizations of deductive reasoning common to the systems of Hilbert, Frege, and Russell (see, e.g., Hilbert system). Such axiomatizations were most famously used by Russell and Whitehead in their mathematical treatise Principia Mathematica. Spurred on by a series of seminars in Poland in 1926 by Łukasiewicz that advocated a more natural treatment of logic, 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. His proposals led to different notationssuch as Fitch-style calculus (or Fitch's diagrams) or Suppes' method of which e.g. Lemmon gave a variant called system L. Natural deduction in its modern form was independently proposed by the German mathematician Gerhard Gentzen in 1934, in a dissertation delivered to the faculty of mathematical sciences of the University of Göttingen. The term natural deduction (or rather, its German equivalent natürliches Schließen) was coined in that paper: 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 and intuitionistic logic. In a series of seminars in 1961 and 1962 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 was to become a reference work on natural deduction, and included applications for 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 Martin-Löf's description of logical judgments and connectives. A judgment is something that is knowable, that is, an object of knowledge. It is evident if one in fact knows it. Thus 'it is raining' is a judgment, which is evident for the one who knows that it is actually raining; in this case one may readily find evidence for the judgment by looking outside the window or stepping out of the house. In mathematical logic however, evidence is often not as directly observable, but rather deduced from more basic evident judgments. The process of deduction is what constitutes a proof; in other words, a judgment is evident if one has a proof for it. The most important judgments in logic are of the form 'A is true'. The letter A stands for any expression representing a proposition; the truth judgments thus require a more primitive judgment: 'A is a proposition'. Many other judgments have been studied; for example, 'A is false' (see classical logic), 'A is true at time t' (see temporal logic), 'A is necessarily true' or 'A is possibly true' (see modal logic), 'the program M has type τ' (see programming languages and type theory), 'A is achievable from the available resources' (see linear logic), and many others. To start with, we shall concern ourselves with the simplest two judgments 'A is a proposition' and 'A is true', abbreviated as 'A prop' and 'A true' respectively. The judgment 'A prop' defines the structure of valid proofs of A, which in turn defines the structure of propositions. For this reason, the inference rules for this judgment are sometimes known as formation rules. To illustrate, if we have two propositions A and B (that is, the judgments 'A prop' and 'B prop' are evident), then we form the compound proposition A and B, written symbolically as ' A ∧ B {displaystyle Awedge B} '. We can write this in the form of an inference rule: