Formal System Article Index for
Formal
Website Links For
Formal
 

Information About

Formal System




In Mathematics , formal proofs are the product of formal systems, consisting of Axiom s and rules of deduction. Theorems are then recognized as the possible 'last lines' of formal proofs. The point of view that this picture encompasses mathematics has been called Formalist . The term has been used Pejorative ly. On the other hand, David Hilbert founded Metamathematics as a discipline designed for discussing formal systems; it is not assumed that the Metalanguage in which proofs are studied is itself less informal than the usual habits of mathematicians suggest. To contrast with the metalanguage, the language described by a formal grammar is often called an object language (i.e., the object of discussion - this distinction may have been introduced by Carnap ).

It has become common to speak of a formalism, more-or-less synonymously with a formal system ''within standard mathematics'' invented for a particular purpose. This may not be much more than a '''notation''', such as Dirac 's Bra-ket Notation .

Mathematical formal systems consist of the following:
# A finite set of symbols which can be used for constructing formulae.
# A grammar, i.e. a way of constructing well-formed formulae out of the symbols, such that it is possible to find a decision procedure for deciding whether a formula is a well-formed formula (''wff'') or not.
# A set of axioms or axiom schemata: each axiom has to be a ''wff''.
# A set of Inference Rules .
# A set of theorems. This set includes all the axioms, plus all ''wff''s which can be derived from previously-derived theorems by means of rules of inference. Unlike the grammar for ''wff''s, there is no guarantee that there will be a Decision Procedure for deciding whether a given ''wff'' is a theorem or not.