Theorem - Formalized Account of Theorems - Derivation of A Theorem

Derivation of A Theorem

The notion of a theorem is very closely connected to its formal proof (also called a "derivation"). To illustrate how derivations are done, we will work in a very simplified formal system. Let us call ours Its alphabet consists only of two symbols { A, B } and its formation rule for formulas is:

Any string of symbols of which is at least 3 symbols long, and which is not infinitely long, is a formula. Nothing else is a formula.

The single axiom of is:

ABBA

The only rule of inference (transformation rule) for is:

Any occurrence of "A" in a theorem may be replaced by an occurrence of the string "AB" and the result is a theorem.

Theorems in are defined as those formulae which have a derivation ending with that formula. For example

1. ABBA (Given as axiom)
2. ABBBA (by applying the transformation rule)
3. ABBBAB (by applying the transformation rule)

is a derivation. Therefore "ABBBAB" is a theorem of The notion of truth (or falsity) cannot be applied to the formula "ABBBAB" until an interpretation is given to its symbols. Thus in this example, the formula does not yet represent a proposition, but is merely an empty abstraction.

Two metatheorems of are:

Every theorem begins with "A".

Every theorem has exactly two "A"s.