# Formal Systems

Formal Systems are a type of logic based upon deductive reasoning and a formal language. They use a high level of abstraction to remove successive levels of detail and capture the structure of a deductive system of reason in its most basic form within symbolic notation. Examples of formal systems can be found in mathematics, computer science, logic and many other areas. The two central characteristics of a formal system are the usage of deductive reasoning and formal languages. Formal systems – within philosophy, logic, and mathematics – work to infer theorems. They do this by stating a set of axioms, a logical process of reasoning and a formal language. The formal language is then used to compute formulas built up from axioms according to the set of rules specific to that formal system.

### Formal languages

Formal languages are specially constructed symbolic systems, where the vocabulary and rules are precisely and carefully defined. A formal language is normally defined by an alphabet and rules of formation. The alphabet of a formal language is a set of symbols on which the language is built. The formation rules specify which strings of symbols count as well-formed^{1}.

### Alphabet and Syntax

Formal languages consist of an alphabet and a rule for deriving sentences. An alphabet is the set of all symbols used in the language, such a letters, numbers, punctuation etc. The characters in an alphabet are typically denoted as a set in the form ∑={1,2,3,4…}. A string is a particular combination of the letters within an alphabet, if the alphabet was ∑={a,b} then a string may be “ab” or “aaa” or any combination of the letters. Syntax is what gives a language meaning, whereas a string may be any combination of the symbols within that language, syntax is the set of rules that define what combination of letters are valid and which are not. Thus one could create a syntax that did not allow three vowels to follow each other, in such a language “ede” would be a valid expression but “eee” would not. A syntax is not concerned with the validity of a particular statement, it is purely symbolic, they simply define symbolic rules.

### Deductive

Formal systems are more than simply formal languages; we may say formal languages are a subset of formal systems. In addition to an alphabet and a syntax formal systems also have a set of deductive rules, a set of rules of inference and a set of axioms, that are allowed by stipulation.

### Axioms

Axioms are a set of stipulations; a set of statements that are held as self-evident. Axioms form the statements or propositions on which theorems are built. The word axiom comes from the Greek word meaning ‘that which is thought worthy or fit’ or ‘that which commends itself as evident.’^{2} The statement that a line is the shortest distance between two points is an example of an axiom within Euclidean geometry. In mathematics, an axiomatic system is any set of axioms from which some or all axioms can be used in conjunction to logically derive theorems. A mathematical theory consists of an axiomatic system and all its derived theorems^{3}.

To axiomatize a system of knowledge is to show that its claims can be derived from a small, well-understood set of sentences (the axioms). There are typically multiple ways to axiomatize a given mathematical domain. A set of axioms should be consistent; it should be impossible to derive a contradiction from the axiom. A set of axioms should also be non-redundant; an assertion that can be deduced from other axioms need not be regarded as an axiom^{4}. In both senses, an axiom is any mathematical statement that serves as a starting point from which other statements are logically derived.

### Rules of inference

Rules of inference are a set of procedures which combine known facts to infer new facts. For example, given that 1. Kate is a woman and that 2. all women are mortal, we can infer that Kat is mortal. Typically rules of inference are designed to preserve truth, so that as long at the input is valid, then the output can be certain to be valid. These rules of inference are used to generate new knowledge in the form of theorems. Thus rules of inference define the set of logical instructions that take us from the axioms to a theorem. Within formal systems axioms and deductive rules are used to create new theorems. All theorems must be valid strings of the alphabet, and they have to follow from the rules of inference.

### Metalanguage

Formal languages are divided into metalanguages and object languages, where a metalanguage is a language used to describe and talk about the actual formal language. The object language is the language itself which does not contain the terms to refer to its own structure and functioning. An object language is a subset of its metalanguage. The metalanguage may be understood as simply an abstraction of the object language, which includes an added level of abstraction for describing the operations of the original object language.

### Formal Proofs

A formal proof is a finite sequence of well-formed formulas each of which is an axiom or follows from the preceding formulas in the sequence by a rule of inference. The last sentence in the sequence is a theorem of a formal system. Formal proofs are useful because their theorems can be interpreted as true propositions^{5}. Because formal systems are based on deductive logic they have a number of important properties. Firstly: consistency, which means that no theorem of the system contradicts another. Secondly: validity, which means that the system’s rules of proof never allow a false inference from true premises. Thirdly: completeness, which means that if a formula is true, it can be proven, i.e. is a theorem of the system. Fourth: soundness, meaning that if any formula is a theorem of the system, it is true. This is the converse of completeness.

*Complexity Labs*, July 23, 2016, http://complexitylabs.io/formal-systems/.