A Guide to Proof Strategies

Usually, when you are working on a proof, you should use the logical forms of the givens and goals to guide you in choosing what proof strategies to use. Here is a summary of the various forms that givens and goals might take, the strategies that are most appropriate for each form, and how to carry out those strategies in Proof Designer. For a more complete explanation of these strategies, see my book How To Prove It, published by Cambridge University Press.

To Prove a Goal of the Form:

• PQ
  • Assume that P is true and prove Q. To do this in Proof Designer, select the goal and then give the Direct command in the Strategy menu.
  • Prove the contrapositive; i.e., assume that Q is false and prove that P is false. In Proof Designer, select the goal and give the Contrapositive command in the Strategy menu.
• P
  • Reexpress as a positive statement. In Proof Designer, select the goal, give the Reexpress command in the Strategy menu, and use the Reexpress Negative button in the Reexpress dialog box.
  • Use proof by contradiction; i.e., assume P is true and try to reach a contradiction. In Proof Designer, select the goal and give the Contradiction command in the Strategy menu. If you already know which given you are planning to contradict, you can select it too before giving the Contradiction command, and Proof Designer will indicate what you have to prove to achieve the desired contradiction.
• P₁P₂...P_n
  • Prove P₁, P₂, ..., P_n separately. In other words, treat this as a list of n separate goals. In Proof Designer, select the goal and give the Conjunction command in the Infer menu. If you already have some of the statements P₁, P₂, ..., P_n as givens, you can select them too and Proof Designer will only ask you to prove the statements from this list that you don't already know.
• P₁P₂...P_n
  • Assume that all but one of the statements in the list P₁, P₂, ..., P_n are false, and prove that the remaining statement is true. In Proof Designer, select the goal and give the Disjunction command in the Strategy menu. Proof Designer will ask which statement you are planning to prove. If you don't want to assume the negations of the other statements, remove the check mark from the “Assume negations of others” check box by clicking on it.
  • Use proof by cases. In each case, prove one of the statements P₁, P₂, ..., P_n. In Proof Designer, use the Cases command in the Strategy menu to break your proof into cases. Once you have broken the proof into cases, your goal in each case will be P₁P₂...P_n. For each case, select this goal, give the Disjunction command in the Strategy menu, and tell Proof Designer which statement you plan to prove. If you are using this strategy, you probably will want to remove the check mark from the “Assume negations of others” check box.
• PQ
  • Prove PQ and QP, using the methods listed under PQ above. In Proof Designer, select the goal and give the Biconditional command in the Strategy menu.
• xP(x)
  • Let x stand for an arbitrary object, and prove P(x). (If the letter x already stands for something in the proof, you will have to use a different letter for the arbitrary object.) In Proof Designer, select the goal and give the Arbitrary Object command in the Strategy menu.
• xP(x)
  • Find a value of x that makes P(x) true. Prove P(x) for this value of x. In Proof Designer, select the goal and give the Existence command in the Strategy menu. Proof Designer will ask you what value you want to use for x. You have two choices: If you know what value you want to assign to x, select the “Use this value” choice and type in the value. If you don't know what value to use, select the “Use this new variable, whose definition will be inserted later” choice, and type in an unused variable name. In the latter case, you can begin working on the proof of P(x) even before you have decided what value you want to use for x.
• !xP(x)
  • Prove xP(x) (existence) and xy(P(x)P(y)x = y) (uniqueness). In Proof Designer, select the goal and give the Existence & Uniqueness command in the Strategy menu.
  • Prove the equivalent statement x(P(x)y(P(y)y = x)). In Proof Designer, select the goal, give the Reexpress command in the Strategy menu, and click on the Apply Definition button.

To Use a Given of the Form:

• PQ
  • If you are also given P, or you can prove that P is true, then you can conclude that Q is true. In Proof Designer, if you already have P in your givens list then you can select the givens P and PQ and give the Modus Ponens command in the Infer menu. If you don't already have P in the givens list but you think you can prove it, you may want to insert a proof of P at this point in the proof, using the Insert command in the Edit menu.
  • Use the contrapositive: If you are given or can prove that Q is false, you can conclude that P is false. In Proof Designer, select the givens Q and PQ and give the Modus Tollens command in the Infer menu. If necessary, you may first have to insert a proof of Q.
• P
  • Reexpress as a positive statement. In Proof Designer, select the given, give the Reexpress command in the Strategy menu, and use the Reexpress Negative button in the Reexpress dialog box.
  • If you are doing a proof by contradiction, you can reach a contradiction by proving P. In Proof Designer, select the given and give the Contradiction command in the Strategy menu.
• P₁P₂...P_n
  • Treat this as a list of separate givens, P₁, P₂, ..., P_n. In Proof Designer, select the given and give the Split Up command in the Infer menu.
• P₁P₂...P_n
  • Use proof by cases. In case 1 assume P₁ is true, in case 2 assume P₂ is true, etc. In Proof Designer, select the given and give the Cases command in the Strategy menu.
  • If you are also given that some of the statements in the list P₁, P₂, ..., P_n are false, or you can prove that they are false, you can conclude that one of the other statements in the list must be true. In ProofDesigner, select the given P₁P₂...P_n, together with any negations of statements in the list P₁, P₂, ..., P_n that you have in your givens list, and give the Disjunctive Syllogism command in the Infer menu.
• PQ
  • Treat this as two givens: PQ, and QP. In Proof Designer, select the given and give the Split Up command in the Infer menu.
• xP(x)
  • You may plug in any value, say a, for x, and conclude that P(a) is true. In Proof Designer, select the given and give the Universal Instantiation command in the Infer menu. Proof Designer will ask what you want to plug in for x. As with proofs of goals of the form xP(x), if you're not sure what to plug in for x, you can choose a new variable to stand for the object to be plugged in, and fill in the definition of this variable later.
• xP(x)
  • Introduce a new variable, say x₀, into the proof, to stand for a particular object for which P(x₀) is true. In Proof Designer, select the given and give the Existential Instantiation command in the Infer menu.
• !xP(x)
  • Introduce a new variable, say x₀, into the proof, to stand for a particular object for which P(x₀) is true. You may also assume that y(P(y)y = x₀). In Proof Designer, select the given and give the Existential Instantiation command in the Infer menu.

Techniques That Can Be Used in Any Proof

• Proof by contradiction: Assume the goal is false and derive a contradiction. In Proof Designer, select the goal and give the Contradiction command in the Strategy menu. If you already know which given you are planning to contradict, you can select it too before giving the Contradiction command
• Proof by cases: Consider several cases that are exhaustive—i.e., that include all the possibilities. Prove the goal in each case. There are two ways to do this in Proof Designer. If you select a given of the form P₁P₂...P_n and give the Cases command in the Strategy menu, Proof Designer will break the proof into the cases determined by this given. You can also select any goal and give the Cases command, and Proof Designer will ask you to type in some statement P that will be used to distinguish the cases in the proof of this goal. In case 1, Proof Designer will assume that P is true, and in case 2 it will assume that P is false.