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

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

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.