# formal system

In mathematical logic, a formal system is a “set-up” 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. 1.

the language  of $S$, which is formed by

1. (a)

a set $\Sigma$ of symbols; finite sequences  of these symbols are called words or expressions over $\Sigma$;

2. (b)
3. (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. 2.

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

1. (a)

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

2. (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 (well-formed) 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:

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
Title formal system FormalSystem 2013-03-22 19:12:25 2013-03-22 19:12:25 CWoo (3771) CWoo (3771) 15 CWoo (3771) Topic msc 03B99 logical system DeductiveSystem