There are several ways to formally define what a deduction is, given a deductive system. We will explore some of them here.
Deduction as a Sequence
such that is either an axiom, an element of , or as the result of an application of an inference rule to earlier wff’s , where . If is an element of , we call an assumption or a hypothesis. This way of presenting a deduction is said to be linear.
Deductions presented this way are also called deduction sequences or proof sequences. Deductions in Hilbert-style axiom systems are presented this way.
Deduction as a Tree
Alternatively, a deduction can be thought of as a labeled rooted tree. The nodes are labeled by formulas, and for each node with label, say , its immediate predecessors (children) are nodes whose labels are, say which are premises of some inference rule . Deductions presented this way are also called deduction trees or proof trees. In a deduction tree, the labels of the leaves are either the axioms, or assumptions (from some set ), and the label of the root of the tree is the conclusion of the deduction. Below is an example of a deduction tree:
Here, and are assumptions and the corresponding conclusion of some (binary) rule , and is the assumption and is the conclusion of some (unary) rule . Inference rules may be specified as labels of the edges.
Given a deductive system , if is the conclusion of a deduction from a set , we write
If is another set of wff’s, we also write to mean . In addition, if , we write
to mean and respectively. Furthermore, we may also remove the subscript and write
if no confusion arises. When , we also say that is deducible from . The turnstile symbol is also called the deducibility relation.
If a formula is deducible from , we say that is a theorem (of the corresponding deductive system). In symbol, we write
A property of is the following:
if and , then .
In other words, if is a theorem, and can be deduced from , then is also a theorem, which conforms with our intuition. More generally, we have
if and , then .
Remark. We refrain from calling a deduction a proof. As we have seen earlier, deductions are mathematical abstractions of proofs. So they are mathematical constructed, viewed either as sequences or trees (of formulas). On the other hand, in the literature, “proof” is usually reserved to be used in the meta-language, as in the “proof” of Fermat’s Last Theorem, etc…
|Date of creation||2013-03-22 19:12:53|
|Last modified on||2013-03-22 19:12:53|
|Last modified by||CWoo (3771)|