# Derivation (logic)

A derivation , derivation , or deduction in logic is the extraction of statements from other statements. In doing so, final rules are applied to premises in order to arrive at conclusions . Which final rules are allowed is determined by the calculation used .

The derivation, together with the semantic inference, is one of the two logical methods of arriving at the conclusion.

## Example: propositional and predicate logic

The sequence calculus deals with the derivation of sequences of the shape with the help of the sequence rules . As an illustration, we take the derivation of the sentence about the excluded third party . The rules used are described in the rules of the sequential calculus of the first-order predicate logic . ${\ displaystyle \ Gamma \ varphi}$${\ displaystyle (Ann), (\ vee -Kon1), (\ vee -Kon2), (FU)}$

{\ displaystyle {\ begin {alignedat} {3} {\ text {1. Derivation step:}} \ quad & \ varphi \ varphi & \ quad & (Ann) \\ {\ text {2. Derivation step:}} \ quad & \ varphi (\ varphi \ vee \ neg \ varphi) & \ quad & (\ vee -Con1): \, 1. \\ {\ text {3. Derivation step:}} \ quad & \ neg \ varphi \ neg \ varphi & \ quad & (Ann) \\ {\ text {4. Derivation step:}} \ quad & \ neg \ varphi (\ varphi \ vee \ neg \ varphi) & \ quad & (\ vee -Con2): \, 3. \\ {\ text {5. Derivation step:}} \ quad & (\ varphi \ vee \ neg \ varphi) & \ quad & (FU): \, 2., 4. \ End {alignedat}}}

The following new sequence rule was thus derived:

${\ displaystyle \ quad \ left (AD \ right) \ qquad {\ frac {} {\ varphi \ vee \ neg \ varphi}}}$

It can now be used just like the basic rules of calculus.

## The derivability relation and the derivability operator

### definition

To formalize the derivability is often derivative operator (also inference) is used which on the derivation relationship (also Inferenzrelation ) is defined. ${\ displaystyle \ vdash}$

If - according to the rules of a concrete calculus - the expression (the conclusion or the consequence) can be derived from the set (the premises) in finitely many steps, one writes for it ; here is the derivative relation . ${\ displaystyle \ varphi}$${\ displaystyle \ Theta}$${\ displaystyle \ Theta \ vdash \ varphi}$${\ displaystyle \ vdash}$

This derivability relation (also inferential relation ) is a relation between a set of statements, the premises, and a single statement, the conclusion. is to be read as: " can be derived from ". ${\ displaystyle \ Theta \ vdash \ varphi}$${\ displaystyle \ varphi}$${\ displaystyle \ Theta}$

If one adds all expressions which can be derived from to a given set of expressions (one says that one forms the deductive closure), then the derivative operator (also inference operation ) is defined: ${\ displaystyle \ Theta}$${\ displaystyle \ Theta}$${\ displaystyle H}$${\ displaystyle H (\ Theta) = \ {\ varphi | \ Theta \ vdash \ varphi \}}$

Different logics each define a different concept of derivability. There is a propositional concept of derivability, a predicate logic , an intuitionistic , a modal logic , etc.

### Properties of derivative operators

There are a number of properties that most of the derivability relations (at least those mentioned above) have in common

• Inclusion: (Every assumption is also a consequence).${\ displaystyle \ Theta \ cup \ {\ varphi \} \ vdash \ varphi}$
• Idempotence: if and , then (adding inferences to the assumptions does not lead to new conclusions.)${\ displaystyle \ Theta \ vdash \ varphi}$${\ displaystyle \ Theta \ cup \ {\ varphi \} \ vdash \ psi}$${\ displaystyle \ Theta \ vdash \ psi}$
• Monotony : If , then (adding assumptions preserves the consequences possible so far.)${\ displaystyle \ Theta \ vdash \ varphi}$${\ displaystyle \ Theta \ cup \ Delta \ vdash \ varphi}$
• Compactness ; If so , then there is a finite set with such that . (Every conclusion from an infinite set of assumptions can already be reached from a finite subset .)${\ displaystyle \ Theta \ vdash \ varphi}$${\ displaystyle \ Delta}$${\ displaystyle \ Delta \ subseteq \ Theta}$${\ displaystyle \ Delta \ vdash \ varphi}$

From the first three of these properties it can be deduced that an envelope operator is; H. an extensive , monotonous , idempotent mapping . ${\ displaystyle H}$