Short proofs for tricky formulas (Q800909)

The object of this paper is to demonstrate how certain tricky mathematical arguments can be encoded as short formal proofs for the propositional tautologies representing the mathematical statements. Using resolution as a base proof system for the propositional calculus, we exhibit these short proofs under resolution augmented by one of two principles: the principle of extension, originally suggested by Tseitin, and the principle of symmetry, introduced in this paper. These short proofs illustrate the power of extension and symmetry in theorem proving. The principle of extension allows the introduction of auxiliary variables to represent intermediate formulas so that the length of a proof can be significantly reduced by manipulating these variables instead of the formulas that they stand for. Symmetry, on the other hand, allows one to recognize that a tautology remains invariant under certain permutations of variable names, and use that information to avoid repeated independent derivations of intermediate formulas that are merely permutational variants of one another. First we show that a number of inductive arguments can be encoded as short formal proofs using either extension or symmetry. We provide the details for the tautologies derived by encoding the statement, ''An acyclic digraph on n vertices must have a source.'' We then consider the familiar checkerboard puzzle which asserts that a checkerboard, two of whose diagonally opposite corner squares are removed, cannot be perfectly covered with dominoes. We demonstrate short proofs for the tautologies derived from the above assertion, using extension to mimic the tricky informal argument. Finally, we consider statements asserting the Ramsey property of numbers much larger than the critical Ramsey numbers. We show that the proof of Ramsey's theorem can be imitated using the principle of symmetry to yield short proofs for these tautologies. The main theme of the paper is that both extension and symmetry are very powerful augmentations to resolution. We leave open wether either extension or symmetry can polynomially simulate the other.