# Post canonical system

A **Post canonical system** is a formalism for modelling logical theories, developed by Emil Post in the 1930's.

A Post canonical system contains a set called *axioms*, which are strings over a given alphabet of symbols. It also contains a set of *productions*, each of which contains a *antecedent* and a *consequent*. Each of these is what we would think of as "patterns" nowadays - a string of symbols from the alphabet, which may also contain "wildcards". Each "wildcard" in the antecedent can match any number of symbols; the corresponding "wildcard" in the consequent is substituted with the thing that was matched.

To *prove* a *conjecture* within a Post canonical system, one starts with one of the axioms and attempts to derive the conjecture by repeatedly applying the productions to it. In this way, a Post canonical system describes a formal language - the set of conjectures (strings) which the system can prove (generate).

## Example[edit]

For example, take the following axiom:

()

and the following productions:

1.n→ (n) 2.n→n()

and say we want to prove or disprove the conjecture

(()())

We can start with the axiom

()

apply production 2 to yield

()()

and then apply production 1 to yield

(()())

thus proving the conjecture.

## Computational class[edit]

Post canonical systems have been shown to be in the same computational class as Turing machines, that is, they are Turing-complete. They can be seen as (probably) the first approach to string-rewriting.

Post canonical systems can have further restrictions imposed upon them and still be Turing-complete. Post normal systems, for example, can only have one "wildcard" in each production - at the end of the antecedent and the beginning of the consequent. Tag systems are even more restricted than that.