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 picture encompasses mathematics has been called formalist. The term has been used pejoratively. 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, that is, the object of discussion.

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:

1. A finite set of symbols which can be used for constructing formulae.
2. 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.
3. A set of axioms or axiom schemata: each axiom has to be a wff.
4. A set of inference rules.
5. 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.

Formal languages | Mathematical logic | Formal methods | Systems

Metasprache | Sistema formal | Métalangage | Metajęzyk