   Go backward to B.2 PreliminariesGo up to B Proving PropositionsGo forward to B.4 Decomposing the Goal ## B.3 General Strategies

Direct Proof  Given some knowledge K, the usual situation is that we want to find out whether a formula G is true or not, i.e., we don't know the truth of G in advance. Therefore we have two possibilities of a  direct proof:
1. We try
 K G
. If we are successful, then G holds.
2. We try
 K ~G
. If we are successful, then ~G holds.

If the first proof does not work out, it may give sufficient insight in order to establish the second proof. If we can show ~G, we may have gained additional insight that enables us to transform G into some G' whose validity we can actually prove.

Indirect Proof  If we are not successful with direct attempts, we may try an  indirect proof where the goal is to derive a  contradiction.

Proposition 140 (Proof by Contradiction) For proving with knowledge K the goal G, it suffices to prove F(alse) with additional knowledge ~G.
 K G
~~>
 K union {~G} F(alse)

In natural language, a proof of G by contradiction is usually indicated as

We assume ~G and show a contradiction.

A contradiction is usually derived by establishing a proof situation

 K union {G, ~G} F(alse)
because we then immediately have
 K union {G, ~G} F(alse)
~~>
 K union {F(alse)} F(alse)
~~>
 K union {F(alse)}
.

Examples of such proofs are given in the proof of the Peano laws from the set-theoretic construction of the natural numbers or the proof that the square root of 2 is not a rational number.

Again, since we don't know the truth of G for sure, we generally we have two possibilities:

1. We try
 K union {~G} F(alse)
. If we are successful, then G holds.
2. We try
 K union {G} F(alse)
. If we are successful, then ~G holds.

If all attempts have failed, we have hopefully gained more insight to start a new round of attempts with refined ideas.

Proof Directions  When pursuing a proof, we may proceed in two ways:

1. Top-Down by decomposing the goal into simpler formulas with corresponding subproofs.
 K G
~~>
 K0 G0
...
 Kn-1 Gn-1
2. Bottom-Up by deriving new knowledge from the given knowledge such that the goal ultimately becomes part of the knowledge.
 K G
~~>
 K union {F} G

In the course of a proof we mix top-down steps with bottom-up steps; usually we begin with the top-down strategy.

Author: Wolfgang Schreiner
Last Modification: October 4, 1999   