Namespaces
Variants
Actions

Difference between revisions of "Derivation, logical"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
(TeX)
 
Line 1: Line 1:
 +
{{TEX|done}}
 
A formal derivation in a [[Calculus|calculus]] which involves logical rules, and the main outcome of which is a [[Formula|formula]] interpreted as a [[Proposition|proposition]]; see [[Logical calculus|Logical calculus]]; [[Logico-mathematical calculus|Logico-mathematical calculus]]. Since such calculi are usually endowed with a [[Semantics|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.
 
A formal derivation in a [[Calculus|calculus]] which involves logical rules, and the main outcome of which is a [[Formula|formula]] interpreted as a [[Proposition|proposition]]; see [[Logical calculus|Logical calculus]]; [[Logico-mathematical calculus|Logico-mathematical calculus]]. Since such calculi are usually endowed with a [[Semantics|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|Derivation rule]]), one says that the sequence of formulas is a derivation (of its last term <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d0312201.png" />) from the hypotheses <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d0312202.png" /> (<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d0312203.png" />), 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d0312204.png" />. Formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d0312205.png" /> is then called derivable from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d0312206.png" />. If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d0312207.png" />, the notation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d0312208.png" /> means that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d0312209.png" /> is derivable in the relevant calculus without any assumptions; the notation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122010.png" />, which means that "the assumptions A1…An lead to a contradiction" , is also employed (in most systems being studied <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122011.png" /> means that any formula at all may be deduced from these hypotheses). For instance, in a calculus containing the axiom <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122012.png" /> and the rule of [[Modus ponens|modus ponens]], the sequence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122013.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122014.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122015.png" />, is a derivation of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122016.png" /> from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122017.png" /> (i.e. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122018.png" />). The following are properties of logical derivability: <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122019.png" />; if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122020.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122021.png" />; if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122022.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122023.png" />; if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122024.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122025.png" />; if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122026.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122027.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122028.png" /> (here <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122029.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122030.png" /> are formulas, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122031.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122032.png" /> are lists of formulas and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122033.png" /> 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|Derived rule]]; [[Deducible rule|Deducible rule]]), render systems with the symbol <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122034.png" /> much like a [[Gentzen formal system|Gentzen formal system]]. In calculi based on classical logic, a characteristic property is <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122035.png" />. In intuitionistic logic (constructive logic) it is possible to demonstrate, under certain assumptions on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122036.png" />, the principles of Brouwer's concept of derivability: 1) if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122037.png" />, then either <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122038.png" /> or <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122039.png" />; and 2) if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122040.png" />, then, for some term <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122041.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122042.png" /> (these assumptions are invariably met for the empty <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031220/d03122043.png" />). Possibilities of discarding certain assumptions, including transitions to conclusions without any hypotheses, are governed by a [[Deduction theorem|deduction theorem]].
+
If the axioms and the rules of logical transitions are given (cf. [[Derivation rule|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|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|Derived rule]]; [[Deducible rule|Deducible rule]]), render systems with the symbol $\vdash$ much like a [[Gentzen formal system|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|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|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 completeness theorem]]; [[Gödel incompleteness 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|Natural logical deduction]]).
 
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|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 completeness theorem]]; [[Gödel incompleteness 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|Natural logical deduction]]).

Latest revision as of 10:29, 11 October 2014

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)
How to Cite This Entry:
Derivation, logical. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Derivation,_logical&oldid=11644
This article was adapted from an original article by S.Yu. Maslov (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article