Formal Systems
A formal system (or deductive system) is an abstract structure and formalization of an axiomatic system used for deducing, using rules of inference, theorems from axioms.
In 1921, David Hilbert proposed to use formal systems as the foundation of knowledge in mathematics. However, in 1931 Kurt Gödel proved that any consistent formal system sufficiently powerful to express basic arithmetic cannot prove its own completeness. This effectively showed that Hilbert's program was impossible as stated.
The term formalism is sometimes a rough synonym for formal system, but it also refers to a given style of notation, for example, Paul Dirac's bra–ket notation.
Components
A formal system has the following components, as a minimum:
- Formal language, which is a set of well-formed formulas, which are strings of symbols from an alphabet, formed by a formal grammar (consisting of production rules or formation rules).
- Deductive system, deductive apparatus, or proof system, which has rules of inference that take axioms and infers theorems, both of which are part of the formal language.
- In some cases also an inductive system, used to derive a proof by first establishing a simple case, then generalizing it
Formal language
A formal language is a language that uses a set of strings whose symbols are taken from a specific alphabet, and operations used to form sentences from them. Like languages in linguistics, formal languages generally have two aspects:
- the syntax is what the language looks like (more formally: the set of possible expressions that are valid utterances in the language)
- the semantics are what the utterances of the language mean (which is formalized in various ways, depending on the type of language in question)
Usually only the syntax of a formal language is considered via the notion of a formal grammar. The two main categories of formal grammar are that of generative grammars, which are sets of rules for how strings in a language can be written, and that of analytic grammars (or reductive grammar), which are sets of rules for how a string can be analyzed to determine whether it is a member of the language.
Deductive system
A deductive system, also called a deductive apparatus, consists of the axioms (or axiom schemata) and rules of inference that can be used to derive theorems of the system.
In order to sustain its deductive integrity, a deductive apparatus must be definable without reference to any intended interpretation of the language. The aim is to ensure that each line of a derivation is merely a logical consequence of the lines that precede it. There should be no element of any interpretation of the language that gets involved with the deductive nature of the system.
The logical consequence (or entailment) of the system by its logical foundation is what distinguishes a formal system from others which may have some basis in an abstract model. Often the formal system will be the basis for or even identified with a larger theory or field (e.g. Euclidean geometry) consistent with the usage in modern mathematics such as model theory.
An example of a deductive system would be the rules of inference and axioms regarding equality used in first order logic.
The two main types of deductive systems are proof systems and formal semantics.