Proof lengths in logic
As discussed on page 1170 equivalence between expressions can always be proved by transforming to and from canonical form. But with n variables a DNF-type canonical form can be of size 2n—and can take up to at least 2n proof steps to reach. And indeed if logic proofs could in general be done in a number of steps that increases only like a polynomial in n this would mean that the NP-complete problem of satisfiability could also be solved in this number of steps, which seems very unlikely (see page 768).
In practice it is usually extremely difficult to find the absolute shortest proof of a given logic theorem—and the exact length will depend on what axiom system is used, and what kinds of steps are allowed. In fact, as mentioned on page 1155, if one does not allow lemmas some proofs perhaps have to become exponentially longer. The picture below shows in each of the axiom systems from page 808 the lengths of the shortest proofs found by a version of Waldmeister (see page 1158) for all 582 equivalences (see page 818) that involve two variables and up to 3 Nands on either side.
The longest of these are respectively {57, 94, 42, 57, 55, 53, 179, 157} and occur for theorems
{(((a ⊼ a) ⊼ b) ⊼ b) (((a ⊼ b) ⊼ a) ⊼ a), (a ⊼ (a ⊼ (a ⊼ a))) (a ⊼ ((a ⊼ b) ⊼ b)), (((a ⊼ a) ⊼ a) ⊼ a) (((a ⊼ a) ⊼ b) ⊼ a), (((a ⊼ a) ⊼ b) ⊼ b) (((a ⊼ b) ⊼ a) ⊼ a), (a ⊼ ((b ⊼ b) ⊼ a)) (b ⊼ ((a ⊼ a) ⊼ b)), ((a ⊼ a) ⊼ a) ((b ⊼ b) ⊼ b), ((a ⊼ a) ⊼ a) ((b ⊼ b) ⊼ b), ((a ⊼ a) ⊼ a) ((b ⊼ b) ⊼ b)}
Note that for systems that do not already have it as an axiom, most theorems use the lemma (a ⊼ b) (b ⊼ a) which takes respectively {6, 1, 8, 49, 8, 1, 119, 118} steps to prove.