formal system (original) (raw)

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
   2. (a)
      a set Σ of symbols; finite sequences of these symbols are called words or expressions over Σ;
   3. (b)
   4. (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. 1. a deductive system (or proof system) associated with S, which consists of
   2. (a)
      a set of axioms; each axiom is usually (but not always) a formula;
   3. (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 Σ of symbol. Three sets are associated:

where Σ* is the set of all expressions over Σ, Fmla⁡(S) is the set of all (well-formed) formulas obtained by a set of formula formation rules, and 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 P⁢R⁢O⁢P. The symbols of P⁢R⁢O⁢P consists of

(not including , the symbol for commas, and a set of elements called propositional variables. Formulas of P⁢R⁢O⁢P are generated as follows:

• •
  propositional variables are formulas; and
• •
  if α,β are formulas, so are

A deduction system for P⁢R⁢O⁢P may consist the following:

• •
  all formulas of the forms

  (α→(α→β)),((α→(β→γ))→((α→β)→(α→γ))),((¬(¬α))→α)
  for all formulas α,β, and

• •
  γ, and the (only) rule of inference is modus ponens: from α and (α→β), we may infer (or deduce) β.

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.

References

• 1 R. M. Smullyan,Theory of Formal Systems, Princeton University Press, 1961
• 2 J. R. Shoenfield,Mathematical Logic, AK Peters, 2001