Derivation, logical

A formal derivation in a calculus which involves logical rules, and the main outcome of which is a formula interpreted as a proposition; see Logical calculus; Logico-mathematical calculus. Since such calculi are usually endowed with a semantics, a logical derivation is sometimes understood to mean a meaningful statement permitting to pass from formulated axioms and hypotheses (assumptions) to new propositions which are a logical consequence of the starting ones.

If the axioms and the rules of logical transitions are given (cf. Derivation rule), one says that the sequence of formulas is a derivation (of its last term $A$) from the hypotheses $A_1,\dots,A_n$ ($n\geq0$), if each term of the sequence is an axiom, is one of the hypotheses or else may be obtained from the preceding formulas in accordance with one of the rules. This is written as $A_1,\dots,A_n\vdash A$. Formula $A$ is then called derivable from $A_1,\dots,A_n$. If $n=0$, the notation $\vdash A$ means that $A$ is derivable in the relevant calculus without any assumptions; the notation $A_1,\dots,A_n\vdash$, which means that "the assumptions $A_1,\dots,A_n$ lead to a contradiction", is also employed (in most systems being studied $A_1,\dots,A_n\vdash$ means that any formula at all may be deduced from these hypotheses). For instance, in a calculus containing the axiom $A\supset(B\supset A)$ and the rule of modus ponens, the sequence $A$, $A\supset(B\supset A)$, $B\supset A$, is a derivation of $B\supset A$ from $A$ (i.e. $A\vdash(B\supset A)$). The following are properties of logical derivability: $A\vdash A$; if $\Gamma\vdash\Delta$, then $A,\Gamma\vdash\Delta$; if $A,A,\Gamma\vdash\Delta$, then $A,\Gamma\vdash\Delta$; if $\Gamma,A,B,\Gamma'\vdash\Delta$, then $\Gamma,B,A,\Gamma'\vdash\Delta$; if $\Gamma\vdash A$ and $A,\Gamma'\vdash\Delta$, then $\Gamma,\Gamma'\vdash\Delta$ (here $A$ and $B$ are formulas, $\Gamma$ and $\Gamma'$ are lists of formulas and $\Delta$ is a formula or the empty word). These formulas make a substantial transformation of the list of hypotheses possible and, in conjunction with the rules of introduction and elimination of logical symbols (cf. Derived rule; Deducible rule), render systems with the symbol $\vdash$ much like a Gentzen formal system. In calculi based on classical logic, a characteristic property is $\neg\neg A\vdash A$. In intuitionistic logic (constructive logic) it is possible to demonstrate, under certain assumptions on $\Gamma$, the principles of Brouwer's concept of derivability: 1) if $\Gamma\vdash A\lor B$, then either $\Gamma\vdash A$ or $\Gamma\vdash B$; and 2) if $\Gamma\vdash\exists xA(x)$, then, for some term $t$, $\Gamma\vdash A(t)$ (these assumptions are invariably met for the empty $\Gamma$). Possibilities of discarding certain assumptions, including transitions to conclusions without any hypotheses, are governed by a deduction theorem.

The formulation of the concept of a derivation (and of the systems in terms of which this concept is meaningful) heralded the advent of modern mathematical logic. The modern, more rigorous interpretation of the axiomatic method, in which not only axioms but also logical tools are formalized, made it possible to give a mathematical definition of the concept of a proof and of studying proofs by mathematical methods (cf. Proof theory). The concept of a formal derivation proved to be a good approximation to the concept of a mathematical proof (cf. Gödel completeness theorem; Gödel incompleteness theorem). The artefact formalization of logical deducibility subsequently came nearer to the real methods of meaningful mathematical reasoning (cf. Natural logical deduction).

References

[1]	S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)
[2]	, Mathematical theory of logical deduction , Moscow (1967) (In Russian; translated from English) (Collection of translations)