The resonance strategy

Especially in mathematics and in logic, lemmas (basic truths) play a key role for proving theorems. In ring theory, for example, a useful lemma asserts that, for all elements x, the product in either order of 0 and x is 0; in two-valued sentential (or propositional) calculus, a useful lemma asserts that, for all x, x implies x. Even in algorithm writing and in circuit design, lemmas play a key role: minus(minus(x)) = x in the former and NOT(AND(x,y)) = OR(NOT(x),NOT(y)) in the latter. Whether the object is to prove a theorem, write an algorithm, or design a circuit, and whether the assignment is given to a person or (preferably) to an automated reasoning program, the judicious use of lemmas often spells the difference between success and failure. In this article, we focus on what might be thought of as a generalization of the concept of lemma, namely, the concept of resonator, and on a strategy, the resonance strategy, that keys on resonators. For example, where in Boolean groups—those in which the square of every x is the identity element e—the lemmas yzyz = e and yyzz = e are such that neither generalizes the other, the resonator (formula schema) * * ** = e, by using each occurrence of “star” to assert the presence of some variable, generalizes and captures (in a manner that is discussed in this article) both lemmas. Note that the cited resonator, if viewed as a lemma with star replaced by some chosen variable, captures neither cited lemma as an instance. Lemmas of a theory are provably “true” in the theory and, therefore, can be used to complete an assignment. In contrast, resonators, which capture collections of equations or collections of formulas that may or may not include truths, are used by the resonance strategy to direct the search for the information needed for assignment completion. In addition to discussing how one finds useful resonators, we detail various successes, in some of which the resonance strategy played a key role in obtaining a far better proof and in some of which the resonance strategy proved indispensable. The successes are taken from group theory, Robbins algebra, and various logic calculi.