Formal system
From Wikipedia, the free encyclopedia
In logic and mathematics, a formal system consists of two components, a formal language plus a set of inference rules or transformation rules. A formal system may be formulated purely abstractly, for its own sake, or it may be intended to serve as a description of some domain of real phenomena or some aspect of objective reality.
In mathematics, formal proofs are the product of formal systems, consisting of axioms and rules of deduction. Theorems are then recognized as the possible 'last lines' of formal proofs. The point of view that this sums up all there is to mathematics is often called formalism, but is more properly referred to finitism. David Hilbert founded metamathematics as a discipline for discussing formal systems. Any language that one uses to talk about a formal system is called a metalanguage. The metalanguage may be nothing more than ordinary natural language, or it may be partially formalized itself, but it is generally less completely formalized than the formal language component of the formal system under examination, which is then called the object language, that is, the object of the discussion in question.
Some theorists use the term formalism as a rough synonym for formal system, but the term is also used to refer to a particular style of notation, for example, Paul Dirac's bra-ket notation.
Formal systems in mathematics consist of the following elements:
- 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 wffs which can be derived from previously-derived theorems by means of rules of inference. Unlike the grammar for wffs, there is no guarantee that there will be a decision procedure for deciding whether a given wff is a theorem or not.
