Short proofs for tricky formulas

Reviewer: Gregory E. Minc

Several types of propositional formulas are known that have short proofs in terms of new notions, but no (known) short direct proofs (by resolution rule) using only notions present in the text of the formula. The author of this paper adds new examples to this stock. Two ways of introducing new notions (i.e., indirect deduction rules) are considered. The extension rule (widely studied before) allows the introduction of new variables to stand for complex formulas expressing new notions; the symmetry rule allows one to derive formula sF from F if s is a permutation of propositional variables preserving the set of assumptions from which F is derived. Among the examples considered are “every finite transitive directed graph without 2-cycles must have a source,” “a checkerboard, two of whose diagonally opposite corners are removed, cannot be covered with dominoes,” and some finite Ramsay theorems. There are no proofs of any lower bounds for direct derivations. Nothing seems to be known of the relative strength of the extension and symmetry rules. Dantzin, who introduced the symmetry rule in [1] (which was apparently not known to the author), proved that symmetry (even under permutation defined on literals) can be polynomially simulated by the substitution rule.