deduction


DeductionsMathworldPlanetmathPlanetmath are formalizations of proofs. Informally, they can be viewed as arriving at a conclusionMathworldPlanetmath from a set of assumptions, via applications of some prescribed rules in a finite number of steps.

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

Given a deductive system, a deduction from a set Δ of (well-formed) formulasMathworldPlanetmathPlanetmath can be thought of as a finite sequencePlanetmathPlanetmath of wff’s

A1,A2,,An

such that Ai is either an axiom, an element of Δ, or as the result of an application of an inference rule R to earlier wff’s Ai1,,Aik, where i1,,ik<i. If Ai is an element of Δ, we call Ai an assumption or a hypothesisMathworldPlanetmath. 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 treeMathworldPlanetmath. The nodes are labeled by formulas, and for each node with label, say Y, its immediate predecessors (children) are nodes whose labels are, say X1,,Xn which are premises of some inference rule R. 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:

.25.25Z.75.75YX1.75.75.85826772X2

Here, X1 and X2 are assumptions and Y the corresponding conclusion of some (binary) rule R, and Y is the assumption and Z is the conclusion of some (unary) rule S. Inference rules may be specified as labels of the edges.

Deductions in deduction systems such as natural deduction or sequent calculus are presented this way. In those systems, the edges of the trees are replaced by horizontal lines, dividing premises and conclusions, and rules are sometimes specified next to the lines, in the following fashion:

  X1         X2   R                Y                S                Z

Deducibility Relation

Given a deductive system D, if B is the conclusion of a deduction from a set Δ, we write

ΔDB.

If Γ is another set of wff’s, we also write Δ,ΓDB to mean ΔΓDB. In additionPlanetmathPlanetmath, if Γ={A1,,An}, we write

A1,,AnDB  and  Δ,A1,,AnDB

to mean ΓDB and ΔΓDB respectively. Furthermore, we may also remove the subscript D and write

ΔB

if no confusion arises. When ΔB, we also say that B is deducible from Δ. The turnstile symbol is also called the deducibility relation.

If a formula A is deducible from , we say that A is a theoremMathworldPlanetmath (of the corresponding deductive system). In symbol, we write

DA  or  A.

A property of is the following:

if A and AB, then B.

In other words, if A is a theorem, and B can be deduced from A, then B is also a theorem, which conforms with our intuition. More generally, we have

if ΔA and Γ,AB, then Δ,ΓB.

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…

References

  • 1 A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, 2nd Edition, Cambridge University Press, 2000
  • 2 D. Dalen, Logic and StructureMathworldPlanetmath, 4th Edition, Springer, 2008
Title deduction
Canonical name Deduction
Date of creation 2013-03-22 19:12:53
Last modified on 2013-03-22 19:12:53
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 12
Author CWoo (3771)
Entry type Definition
Classification msc 03F03
Classification msc 03B99
Classification msc 03B22
Synonym proof tree
Synonym proof sequence
Synonym hypothesis
Defines deduction tree
Defines deduction sequence
Defines deducible
Defines deducibility relation
Defines assumption