A deductive system is a formal (mathematical) setup of reasoning. In order to describe a deductive system, a (formal) language system must first be in place, consisting of (well-formed) formulas, strings of symbols constructed according to some prescribed syntax. With the language in place, reasoning, from a formal point of view, is just derivation of a formula, called a conclusion, from a given set of formulas, called assumptions, via a set of formulas, called axioms, and rules, called rules of inference.
More specifically, given a language of well-formed formulas, a deductive system consists of
a set of formulas in called axioms, and
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 (of well-formed formulas). There are four main formulations of deductive systems:
natural deduction: as opposed to a Hilbert system, a natural deduction system consists of all rules and no axioms, so that the focus is on deductions from assumptions. One special aspect about some of the inference rules is the allowance to cancel assumptions, so that theorems are conclusions from those deductions where all of the premises may be cancelled.
Gentzen system, or sequent system: unlike the last two systems, where axioms and inference rules are based on formulas from , in a Gentzen system, the building blocks of axioms and inference rules are sequents, which are expressions of the form
where and are finite sequences of formulas (in , and is a symbol not in . In a Gentzen system, all axioms are of the form , for each formula in . Theorems in a Gentzen system are those formulas (in ) such that is the conclusion of a deduction.
tableau system: in a tableau system, like natural deduction, there are only inference rules and no axioms. However, unlike all of the systems above, the rules are not relations, but labeled trees, which are used to construct larger labeled trees called tableaux from given formulas. Theorems are those formulas corresponding to tableaux satisfying a certain property (namely, being closed).
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 , two deductive systems and are deductively equivalent if any theorem deducible from one system is deducible from another. In other words,
There is also a stronger notion of deductive equivalence: is (strongly) deductively equivalent to exactly when
where is a set of formulas, and is a formula, in . Note that strong deductive equivalence implies weak deductive equivalence. On the other hand, if the deduction theorem and its converse hold in both and , then weak also implies strong.
|Date of creation||2013-03-22 19:12:47|
|Last modified on||2013-03-22 19:12:47|
|Last modified by||CWoo (3771)|