# deductive system

## Introduction

More specifically, given a language $L$ of well-formed formulas, a deductive system $D$ consists of

1. 1.

a set of formulas in $L$ called axioms, and

2. 2.

a set of binary relations  on subsets of $L$; each relation  is called a rule of inference, or simply rule; if $R$ is a rule, and $(\Delta,\Gamma)\in R$, we say that from $\Delta$ we infer $\Gamma$ via $R$; elements of $\Delta$ are called premises, and elements of $\Gamma$ are conclusions. Typically, $\Delta$ is assumed finite (and maybe empty), and $\Gamma$ a singleton.

There are also variations to the setup above. Sometimes the formulas are replaced by other expressions (sequents, etc…), sometimes the rules are not relations, but other constructs (trees, etc…)

A deduction system is also called a deduction system or proof system.

The central task of a deduction system is the construction of deductions, which, informally, is the application of inference rules to assumptions (or axioms, if any) to arrive at a conclusion, in a finite number of steps. For more detail, please see this entry (http://planetmath.org/Deduction).

A deductive system together with the underlying language is called a formal system.

## Some Major Formulations of Deductive Systems in Logic

Let us fix a language $L$ (of well-formed formulas). There are four main formulations of deductive systems:

Of the four formulations above, Hilbert systems are most widely used in logic, and are applicable to many types of logics. Natural deduction and Gentzen systems are more amenable to analysis of deductions, and therefore are mainly used in structural proof theory.

Given a language $L$, two deductive systems $D_{1}$ and $D_{2}$ are deductively equivalent if any theorem deducible from one system is deducible from another. In other words,

 $\vdash_{D_{1}}A\qquad\mbox{iff}\qquad\vdash_{D_{2}}A.$

There is also a stronger notion of deductive equivalence: $D_{1}$ is (strongly) deductively equivalent to $D_{2}$ exactly when

 $\Delta\vdash_{D_{1}}A\qquad\mbox{iff}\qquad\Delta\vdash_{D_{2}}A,$

where $\Delta$ is a set of formulas, and $A$ is a formula, in $L$. Note that strong deductive equivalence implies weak deductive equivalence. On the other hand, if the deduction theorem  and its converse  hold in both $D_{1}$ and $D_{2}$, then weak also implies strong.

## References

• 1 A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, 2nd Edition, Cambridge University Press, 2000
• 2 D. Dalen, , 4th Edition, Springer, 2008
• 3 G. Priest, Introduction to Non-Classical Logic: From If to Is, 2nd Edition, Cambridge University Press, 2008
 Title deductive system Canonical name DeductiveSystem Date of creation 2013-03-22 19:12:47 Last modified on 2013-03-22 19:12:47 Owner CWoo (3771) Last modified by CWoo (3771) Numerical id 25 Author CWoo (3771) Entry type Topic Classification msc 03F03 Classification msc 03B99 Classification msc 03B22 Synonym deduction system Synonym proof system Related topic FormalSystem Related topic InferenceRule Related topic LogicalAxiom Defines deductively equivalent