Natural deduction

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"

where the parentheses are omitted to make the inference rule more succinct:

It must be understood that in such rules the objects are propositions. That is, the above rule is really an abbreviation for:

If the truth of a proposition can be established in more than one way, the corresponding connective has multiple introduction rules.

A pervasive operation in mathematical logic is reasoning from assumptions. For example, consider the following derivation:

This derivation does not establish the truth of B as such; rather, it establishes the following fact:

The notion of hypothetical judgment is internalised as the connective of implication. The introduction and elimination rules are as follows.

With hypothetical derivations, we can now write the elimination rule for disjunction:

This is read as: if falsehood is true, then any proposition C is true.

Dually, local completeness says that the elimination rules are strong enough to decompose a connective into the forms suitable for its introduction rule. Again for conjunctions:

The existential quantifier has the introduction and elimination rules:

A discussion of the introduction and elimination forms for higher-order logic is beyond the scope of this article. It is possible to be in-between first-order and higher-order logics. For example, second-order logic has two kinds of propositions, one kind quantifying over terms, and the second kind quantifying over propositions of the first kind.

These types are generalisations of the arrow and product types, respectively, as witnessed by their introduction and elimination rules.

The modal hypotheses have their own version of the hypothesis rule and substitution theorem.

The proposition A ∨ B, which is the succedent of a premise in ∨E, turns into a hypothesis of the conclusion in the left rule ∨L. Thus, left rules can be seen as a sort of inverted elimination rule. This observation can be illustrated as follows:

The correspondence between the sequent calculus and natural deduction is a pair of soundness and completeness theorems, which are both provable by means of an inductive argument.

It is clear by these theorems that the sequent calculus does not change the notion of truth, because the same collection of propositions remain true. Thus, one can use the same proof objects as before in sequent calculus derivations. As an example, consider the conjunctions. The right rule is virtually identical to the introduction rule

The left rule, however, performs some additional substitutions that are not performed in the corresponding elimination rules.