## 5.1 IntroductionDirect deduction has the merit of being simple to understand. Unfortunately, as we have seen, the proofs can easily become unwieldy. The deduction theorem helps. It assures us that, if we have a proof of a conclusion form premises, there is a proof of the corresponding implication. However, that assurance is not itself a proof. We begin this lesson with a discussion of conditional proofs. We then show how they are combined in the popular ## 5.2 Conditional Proofs
As an example, consider the conditional proof shown below. It resembles a direct proof except that we have grouped the sentences on lines 3 through 5 into a subproof within our overall proof.
The main benefit of conditional proofs is that they allow us to prove things that cannot be proved using only ordinary rules of inference. In conditional proofs, we can make assumptions within subproofs; we can prove conclusions from those assumptions; and, from those derivations, we can derive implications outside of those subproofs, with our assumptions as antecedents and our conclusions as consequents. The conditional proof above illustrates this. On line 3, we begin a subproof with the assumption that As this example illustrates, there are three basic operations involved in creating useful subproofs - (1) making assumptions, (2) using ordinary rules of inference to derive conclusions, and (3) using conditional rules of inference to derive conclusions outside of subproofs. Let's look at each of these operations in turn. In a conditional proof, it is permissible to make an arbitrary assumption in any subproof. The assumptions need not be members of the initial premise set. Note that such assumptions cannot be used directly outside of the subproof, only as conditions in derived implications, so they do not contaminate the superproof or any unrelated subproofs. For example, in the proof we just saw, we used this assumption operation in the nested subproof even though An ordinary rule of inference applies to a particular subproof of a conditional proof if and only if there is an instance of the rule in which all of the premises occur earlier in the subproof or in some superproof of the subproof. Importantly, it is not permissible to use sentences in subproofs of that subproof or in other subproofs of its superproofs. For example, in the conditional proof we have been looking at, it is okay to apply Implication Elimination to 1 and 3. And it is okay to use Implication Elimination on lines 2 and 4. However, it is The last line of the malformed proof shown below gives an example of this. It is
The malformed proof shown below is another example. Here, line 8 is illegal because line 4 is not in the current subproof or a superproof of this subproof.
Correctly utilizing results derived in subproofs is the responsibility of a new type of rule of inference. Like an ordinary rule of inference, a conditional rule of inference is a pattern of reasoning consisting of one or more premises and one or more conclusions. As before, the premises and conclusions can be schemas. However, the premises can also include conditions of the form φ ⊢ ψ. The rule in this case is called Implication Introduction, because it allows us to introduce new implications.
Finally, we define a ## 5.3 FitchFitch is a proof system that is particularly popular in the Logic community. It is as powerful as many other proof systems and is far simpler to use. Fitch achieves this simplicity through its support for conditional proofs and its use of conditional rules of inference in addition to ordinary rules of inference. Fitch has ten rules of inference in all. Nine of these are ordinary rules of inference. The other rule (Implication Introduction) is a conditional rule of inference.
In addition to these rules of inference, it is common to include in Fitch proof editors several additional operations that are of use in constructing Fitch proofs. For example, the Premise operation allows one to add a new premise to a proof. The Reiteration operation allows one to reproduce an earlier conclusion for the purposes of clarity. Finally, the Delete operation allows one to delete unnecessary lines. ## 5.4 Soundness And CompletenessIn talking about Logic, we now have two notions - logical entailment and provability. A set of premises logically entails a conclusion if and only if every truth assignment that satisfies the premises also satisfies the conclusion. A sentence is provable from a set of premises if and only if there is a finite proof of the conclusion from the premises. The concepts are quite different. One is based on truth assignments; the other is based on symbolic manipulation of expressions. Yet, for the proof systems we have been examining, they are closely related. We say that a proof system is The Fitch system is sound and complete for the full language. In other words, for this system, logical entailment and provability are identical. An arbitrary set of sentences Δ logically entails an arbitrary sentence φ if and only if φ is provable from Δ using Fitch. The upshot of this result is significant. On large problems, the proof method often takes fewer steps than the truth table method. (Disclaimer: In the worst case, the proof method may take just as many or more steps to find an answer as the truth table method.) Moreover, proofs are usually much smaller than the corresponding truth tables. So writing an argument to convince others does not take as much space. ## 5.5 Reasoning TipsThe 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
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
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. ## Recap
## ExercisesExercise 5.1: Given Exercise 5.2: Given ( Exercise 5.3: Given Exercise 5.4: Given Exercise 5.5: Given Exercise 5.6: Use the Fitch System to prove Exercise 5.7: Use the Fitch System to prove ( Exercise 5.8: Use the Fitch System to prove (¬ Exercise 5.9: Given Exercise 5.10: Given Exercise 5.11: Given Exercise 5.12: Use the Fitch System to prove (( Exercise 5.13: Given ¬( Exercise 5.14: Use the Fitch system to prove the tautology ( |