formal system
In mathematical logic, a formal system is a “setup” to study the syntactic structures of statements that we see in everyday mathematics. Thus, instead of looking at the meaning of the statement $1+1=2$, one looks at the expression made up of symbols $1,+,1,=$, and $2$.
Formally, a formal system $S$ consists of the following:

1.
the language^{} of $S$, which is formed by

(a)
a set $\mathrm{\Sigma}$ of symbols; finite sequences^{} of these symbols are called words or expressions over $\mathrm{\Sigma}$;

(b)
a set of expressions called wellformed formulas, or simply formulas^{};

(c)
a set of rules that specify how these words are generated; the set is called the syntax of the language; typically, the rules are

*
certain expressions are singled out, which are called atoms, or atomic formulas

*
a set of rules (inductive in nature) showing how formulas can be formed from other formulas that have already been formed

*

(a)

2.
a deductive system (or proof system) associated with $S$, which consists of

(a)
a set of axioms; each axiom is usually (but not always) a formula;

(b)
a set of rules called rules of inference^{} on $S$; the rules of inferences are used to generate formulas, which are known as theorems of $S$; typically,

*
an axiom is a theorem,

*
a formula that can be formed (or deduced) from other theorems by a rule of inference is a theorem.

*

(a)
Thus, in a formal system $S$, one starts with a set $\mathrm{\Sigma}$ of symbol. Three sets are associated:
$${\mathrm{\Sigma}}^{*}\supseteq \mathrm{Fmla}(S)\supseteq \mathrm{Thm}(S)$$ 
where ${\mathrm{\Sigma}}^{*}$ is the set of all expressions over $\mathrm{\Sigma}$, $\mathrm{Fmla}(S)$ is the set of all (wellformed) formulas obtained by a set of formula formation rules, and $\mathrm{Thm}(S)$ is the set of all theorems obtained from the formulas by a set of rules of inference.
Here’s an example of a formal system: the (classical) propositional logic^{} $PROP$. The symbols of $PROP$ consists of
$$\to ,\mathrm{\neg},(,),$$ 
(not including $,$ the symbol for commas, and a set of elements called propositional variables. Formulas of $PROP$ are generated as follows:

•
propositional variables are formulas; and

•
if $\alpha ,\beta $ are formulas, so are
$$(\mathrm{\neg}\alpha )\mathit{\hspace{1em}\hspace{1em}}\text{and}\mathit{\hspace{1em}\hspace{1em}}(\alpha \vee \beta ).$$
A deduction system for $PROP$ may consist the following:

•
all formulas of the forms
$$(\alpha \to (\alpha \to \beta )),((\alpha \to (\beta \to \gamma ))\to ((\alpha \to \beta )\to (\alpha \to \gamma ))),((\mathrm{\neg}(\mathrm{\neg}\alpha ))\to \alpha )$$ for all formulas $\alpha ,\beta $, and

•
$\gamma $, and the (only) rule of inference is modus ponens^{}: from $\alpha $ and $(\alpha \to \beta )$, we may infer (or deduce) $\beta $.
The (classical) firstorder logic is another example of a formal system. Group theory, number theory (a la Peano arithmetic^{}), theory of partially ordered sets^{}, and set theory^{} (a la ZFC) are other examples of formal systems that are extensively studied.
Remark. A formal system is sometimes called a logical system, although the latter term usually either refers to a formal system where the deducibility relation $\u22a2$ arising out of the associated deductive system satisfies certain properties (for example, $A\u22a2A$ for all wffs, etc…), or a formal system together with a semantical structure^{}.
References
 1 R. M. Smullyan, Theory of Formal Systems, Princeton University Press, 1961
 2 J. R. Shoenfield, Mathematical Logic, AK Peters, 2001
Title  formal system 

Canonical name  FormalSystem 
Date of creation  20130322 19:12:25 
Last modified on  20130322 19:12:25 
Owner  CWoo (3771) 
Last modified by  CWoo (3771) 
Numerical id  15 
Author  CWoo (3771) 
Entry type  Topic 
Classification  msc 03B99 
Synonym  logical system 
Related topic  DeductiveSystem 