Proof Hints

• Use the structure of an expression to guide what proof step to take next.
  • Look for subexpressions that you can replace with equivalent expresssions.
  • Use algebraic and logical properties of logical connectives and quantifiers to rewrite formulae. For example, use the One Point Rule to eliminate the existential; use properties of implication (Section 2) to get rid of implications; use properties about quantifiers to move them outward across connectives.
• Use lemmas and auxiliary definitions to add structure to your proof.
  • Introduce them to avoid repeating the same subexpressions or subproofs. (Sound familiar from your programming experience?)
  • Use them to make your proofs more readable, shorter, and more modular.
• Suppose you have an expression, e, given in terms of an operator f. (In fact you may introduced f yourself following the hint above.)
  • Expand the expression e by replacing f with its definition.
  • Then use properties about operators, g, in f's definition to manipulate and simplify the expanded e.
  • At the end, reintroduce (if convenient or necessary) the original f using its definition (in the other direction).