Chapter 12: The Principle of Computational Equivalence

Section 9: Implications for Mathematics and Its Foundations

Nand tautologies

At each step every possible transformation rule in the axioms is applied wherever it can. New expressions are also created by replacing each possible variable with x y, where x and y are new variables, and by setting every possible pair of variables equal in turn. The longest tautology at step t is

Nest[(# #) (# pt) & , p (p p), t - 1]

whose LeafCount grows like 3t. The distribution of sizes of statements generated at each step is shown below.

Even with the same underlying axioms the tautologies are generated in a somewhat different order if one uses a different strategy—say one based on paramodulation (see page 1156). Pages 818 and 1175 discuss the sequence of all Nand theorems listed in order of increasing complexity.

Image Source Notebooks:

From Stephen Wolfram: A New Kind of Science [citation]