4.2: Direct Proof

Direct Proof

"Brute force" is a term commonly applied to considering all possibilities manually, one at a time, before coming to a conclusion. That works well under simple circumstances but is rarely practical within industrial applications. This section discusses that reality so that you can avoid the "brute force" trap.

3.5.2 Direct Proof

Theoretically, you can prove anything in propositional calculus with truth tables. In fact, the laws of logic stated in Section 3.4 are all theorems. Propositional calculus is one of the few mathematical systems for which any valid sentence can be determined true or false by mechanical means. A program to write truth tables is not too difficult to write; however, what can be done theoretically is not always practical. For example,

\(a, a \to b, b \to c, ..., y \to z \Rightarrow z\)

is a theorem in propositional calculus. However, suppose that you wrote such a program and you had it write the truth table for

\( a \wedge (a \to b) \wedge (b \to c) \wedge ... \wedge (y \to z)) \to z\)

The truth table will have \(2^{26}\) cases. At one million cases per second, it would take approximately one hour to verify the theorem. Now if you decided to check a similar theorem,

\(p_1, p_1 \to p_2,...,p_{99} \to p_{100} \Rightarrow p_{100}\)

you would really have time trouble. There would be \(2^{100} \approx 1.26765 \times 10^{30}\) cases to check in the truth table. At one million cases per second it would take approximately 1.46719 × 10¹⁹ days to check all cases. For most of the remainder of this section, we will discuss an alternate method for proving theorems in propositional calculus. It is the same method that we will use in a less formal way for proofs in other systems. Formal axiomatic methods would be too unwieldy to actually use in later sections. However, none of the theorems in later chapters would be stated if they couldn’t be proven by the axiomatic method.

We will introduce two types of proof here, direct and indirect.

Example 3.5.7: A typical direct proof

This is a theorem: \(p \to r, q \to s, \p \vee q \Rightarrow s \vee r\). A direct proof of this theorem is:

Table 3.5.8: Direct proof of \(p \to r, q \to s, \p \vee q \Rightarrow s \vee r\)

 

Note that □ marks the end of a proof.

 

Example 3.5.7 illustrates the usual method of formal proof in a formal mathematical system. The rules governing these proofs are:

1. A proof must end in a finite number of steps.
2. Each step must be either a premise or a proposition that is implied from previous steps using any valid equivalence or implication.
3. For a direct proof, the last step must be the conclusion of the theorem. For an indirect proof (see below), the last step must be a contradiction.
4. Justification Column. The column labeled “justification” is analogous to the comments that appear in most good computer programs. They simply make the proof more readable.

Example 3.5.9: Two proofs of the same theorem

 Here are two direct proofs of \(\neg p \vee q, s \vee p, \neg q \Rightarrow s\):

Table 3.5.10 Direct proof of \(\neg p \vee q, s \vee p, \neg q \Rightarrow s\)

You are invited to justify the steps in this second proof:

Table 3.5.11: Alternate proof of \(\neg p \vee q, s \vee p, \neg q \Rightarrow s\)

The conclusion of a theorem is often a conditional proposition. The condition of the conclusion can be included as a premise in the proof of the theorem. The object of the proof is then to prove the consequence of the conclusion. This rule is justified by the logical law

\(p \to (h \to c) \Leftrightarrow (p \wedge h) \to c\)

Example 3.5.12: Example of a proof with a conditional conclusion

The following proof of \(p \to (q \to s), \neg r \vee p, q \Rightarrow r \to s\) includes r as a fourth premise. Inference of truth of s completes the proof.

Table 3.5.13: Proof of a theorem with a conditional conclusion.