that they ultimately tend to be equivalent in their computational sophistication—and thus show all sorts of similar phenomena.

And what we will see in this section is while some of these phenomena correspond to known features of mathematics—such as Gödel's Theorem—many have never successfully been recognized.

But just what basic processes are involved in mathematics?

Ever since antiquity mathematics has almost defined itself as being concerned with finding theorems and giving their proofs. And in any particular branch of mathematics a proof consists of a sequence of steps ultimately based on axioms like those of the previous two pages [773, 774].

The picture below gives a simple example of how this works in basic logic. At the top right are axioms specifying certain fundamental equivalences between logic expressions. A proof of the equivalence (p⊼q)(q⊼p) between logic expressions is then formed by applying these axioms in the particular sequence shown.

Proof of the theorem (p ⊼ q)  (q ⊼ p) on the basis of the shorter set of axioms for logic from page 773. The symbol ⊼ stands for Nand, sometimes known as Sheffer stroke. The axioms given here do not immediately say whether Nand is commutative (so that (p ⊼ q)  (q ⊼ p)). But the proof demonstrates that in fact this follows from them. Note that the proof uses the approach common in practical mathematics and in Mathematica of doing direct structural substitutions for terms—not the approach based on logical implications that has traditionally been discussed in typical formal mathematical logic.