Reasoning Tips

The Fitch rules are all fairly simple to use; and, as we discuss in the next section, they are all that we need to prove any result that follows logically from any set of premises. Unfortunately, figuring out which rules to use in any given situation is not always that simple. Fortunately, there are a few tricks that help in many cases.

If the goal has the form (φ ⇒ ψ), it is often good to assume φ and prove ψ and then use Implication Introduction to derive the goal. For example, if we have a premise q and we want to prove (p ⇒ q), we assume p, reiterate q, and then use Implication Introduction to derive the goal.

If the goal has the form (φ ∧ ψ), we first prove φ and then prove ψ and then use And Introduction to derive (φ ∧ ψ).

If the goal has the form (φ ∨ ψ), all we need to do is to prove φ or prove ψ, but we do not need to prove both. Once we have proved either one, we can disjoin that with anything else whatsoever.

If the goal has the form (¬φ), it is often useful to assume φ and prove a contradiction, meaning that φ must be false. To do this, we assume φ and derive some sentence ψ leading to (φ ⇒ ψ). We assume φ again and derive some sentence ¬ψ leading to (φ ⇒ ¬ψ). Finally, we use Negation Introduction to derive ¬φ as desired.

More generally, whenever we want to prove a sentence φ of any sort, we can sometimes succeed by assuming ¬φ, proving a contradiction as just discussed and thereby deriving ¬¬φ. We can then apply Negation Elimination to get φ.

The following two tips suggest useful things we can try based on the form of the premises and the goal or subgoal we are trying to prove.

If there is a premise of the form (φ ⇒ ψ) and our goal is to prove ψ, then it is often useful to try proving φ. If we succeed, we can then use Implication Elimination to derive ψ.

If we have a premise (φ ∨ ψ) and our goal is to prove χ, then we should try proving (φ ⇒ χ) and (ψ ⇒ χ). If we succeed, we can then use Or Elimination to derive χ.

As an example of using these tips in constructing the proof, consider the following problem. We are given p ∨ q and ¬p, and we are asked to prove q. Since the goal is not an implication or a conjunction or a disjunction or a negation, only the last of the goal-based tips applies. Unfortunately, this does not help us in this case. Luckily, the second of the premise-based tips is relevant because we have a disjunction as a premise. To use this all we need is to prove p ⇒ q and q ⇒ q. To prove p ⇒ q, we use the first goal-based tip. We assume p and try to prove q. To do this we use that last goal-based tip. We assume ~q and prove p. Then we assume ~q and prove ¬p. Since we have proved p and ¬p from ¬q, we can infer q. Using Implication Introduction, we then have p ⇒ q. Proving q ⇒ q is easy. Finally, we can apply or elimination to get the desired result.

In general, when trying to generate a proof, it is useful to apply the premise tips to derive conclusions. However, this often works only for very short proofs. For more complex proofs, it is often useful to think backwards from the desired conclusion before starting to prove things from the premises in order to devise a strategy for approaching the proof. This often suggests subproblems to be solved. We can then work on these simpler subproblems and put the solutions together to produce a proofs for our overall conclusion.