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. the language of $S$, which is formed by

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

   2. a set of expressions called well-formed formulas, or simply formulas;

   3. 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

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

   2. 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 $\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 (well-formed) 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) first-order 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 $⊢$ arising out of the associated deductive system satisfies certain properties (for example, $A⊢A$ for all wffs, etc…), or a formal system together with a semantical structure.