You are here
Homeformal system
Primary tabs
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 $\Sigma$ of symbols; finite sequences of these symbols are called words or expressions over $\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

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.

Thus, in a formal system $S$, one starts with a set $\Sigma$ of symbol. Three sets are associated:
$\Sigma^{*}\supseteq\operatorname{Fmla}(S)\supseteq\operatorname{Thm}(S)$ 
where $\Sigma^{*}$ is the set of all expressions over $\Sigma$, $\operatorname{Fmla}(S)$ is the set of all (wellformed) formulas obtained by a set of formula formation rules, and $\operatorname{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,\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
$(\neg\alpha)\qquad\mbox{and}\qquad(\alpha\vee\beta).$
A deduction system for $PROP$ may consist the following:

all formulas of the forms
$(\alpha\to(\alpha\to\beta)),\quad((\alpha\to(\beta\to\gamma))\to((\alpha\to% \beta)\to(\alpha\to\gamma))),\quad((\neg(\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 $\vdash$ arising out of the associated deductive system satisfies certain properties (for example, $A\vdash A$ 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
Mathematics Subject Classification
03B99 no label found Forums
 Planetary Bugs
 HS/Secondary
 University/Tertiary
 Graduate/Advanced
 Industry/Practice
 Research Topics
 LaTeX help
 Math Comptetitions
 Math History
 Math Humor
 PlanetMath Comments
 PlanetMath System Updates and News
 PlanetMath help
 PlanetMath.ORG
 Strategic Communications Development
 The Math Pub
 Testing messages (ignore)
 Other useful stuff
 Corrections