Formal system

deductive system

A calculus in mathematical logic, given by the rules of formation of expressions and of constructing derivations (cf. Derivation, logical) in that calculus. The expressions of a formal system are regarded as purely-formal combinations of symbols; the derivation rules determine in which cases a formal expression $A$ can be deduced from other formal expressions $B_1,\dots,B_n$. If $n=0$, then $A$ is called an axiom. Derivations are either sequences or tree diagrams made up of formal expressions according to the derivation rules. If there are only axioms at the vertices of the derivation tree, then the formal expression at the end of the derivation is said to be deducible (or derivable) in the formal system.

Very interesting formal systems are those for which the language and the concept of derivation satisfy the requirement of effectiveness. This means that there must be an effective procedure for determining whether an arbitrary sequence of symbols is an expression of the formal system or not. The concept of a derivation must satisfy the same requirement. The concept of a deducible expression in effective formal systems is, generally speaking, not effective.

The concept of a formal system is one of the central ones in mathematical logic, and it serves the needs of both mathematical logic itself and related areas of mathematics.

The most important class of formal systems is that of formal first-order theories (see [4]) formalizing some branch of meaningful mathematics. Historically, this class of formal systems arose in connection with the program of D. Hilbert of providing a foundation for mathematics (see Formalism).

The concepts and methods for studying formal systems developed in mathematical logic have found applications in a variety of branches of mathematics, for example in group theory and category theory.

See also Formal mathematical analysis.

References

[1]	D. Hilbert, "Grundlagen der Geometrie" , Springer (1913)
[2]	S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)
[3]	A. Church, "Introduction to mathematical logic" , 1 , Princeton Univ. Press (1956)
[4]	S. MacLane, "Topology and logic as a source of algebra" Bull. Amer. Math. Soc. , 82 : 1 (1976) pp. 1–40