Overview

A formal system is an abstract structure and formalization of an axiomatic system used for inferring theorems from axioms by a set of inference rules. It consists of two components: a formal language and a deductive system.

A formal language comprises of an alphabet and a formal grammar. The grammer has associated rules describing how symbols of the alphabet are manipulated to create well-formed formulas (WFFs). The syntax of a language describes the set of possible expressions that are valid utterances. The semantics of a language describe what these valid utterances actually mean.

A deductive system can be further subcategorized as either a proof system or a logical system. In both cases, the general principle is to define a (possibly empty) set of axioms alongside a set of inference rules that together can be used to infer theorems.

Bibliography