Go backward to B.4 Decomposing the Goal Go up to B Proving Propositions Go forward to B.6 Example

B.5 Deriving New Knowledge

K

G

~~>

K union {F}

G

K union {~F}

G

A proof by case distinction decomposes the "universe of situations" into those where a particular assumption F holds and those where it does not hold:

We have to prove G.

1. Assume F. Then ...(proof of G with additional knowledge F).
2. Assume ~F. Then ...(proof of G with additional knowledge ~F).

Frequently a case distinction is introduced in situations where we have a formula (F₀ \/ ... \/ ...F_n-1) in our knowledge:

K union {F0 \/ ... \/ Fn-1}

G

~~>

K union {F0}

G

...

K union {Fn-1}

G

We have to prove G. Since we know (F₀ \/ ... \/ F_n-1), it suffices to consider the following cases:

• Case F₀: ...(proof of G with additional knowledge F₀).
• ...
• Case F_n-1: ...(proof of G with additional knowledge F_n-1).

An example of a proof with case distinction is the verification of Euclid's Algorithm.

K union {forall x: F}

G

~~>

K union {forall x: F, F[x <- T]}

G

A universal formula (forall x: F) in the knowledge base is a "machine" that takes any T and prodcues additional knowledge F[x <- T]. Whenever we are in need of an arbitrary instance of F in our knowledge base, we can start this machine:

We have to prove G. Since we know (forall x: F), we have F[x <- T] and thus ...(proof of G with additional knowledge F[x <- T]).

Applications of this rule are shown in the proof of Proposition Equality and Subset.

K union {exists x: F}

G

~~>

K union {exists x: F, F[x <- a]}

G

(a not in  K union {G, F})

An existential formula (exists x: F) in the knowledge base is an "engine" which returns a constant a about the only thing we know is F[x <- a]. Whenever we are in need of such a constant, we can invoke the machine:

We have to prove G. Since we know (exists x: F), we have have some a with F[x <- a]. Thus ...(proof of G with additional knowledge F[x <- a] for some new constant a).

The application of this rule is demonstrated in the proof of Proposition Function Composition and the proof that the square root of 2 is not rational.

K

G

~~>

K union F

G

(F holds in every domain in which K holds).

This last rule is a "placeholder" for a number of ways to infer

K

F

1. This has been shown in a previous proof or is shown as a subproof.
2. This holds because F is a propositional consequence of K, i.e., the conclusion holds independently of the truth values of the atomic formulas and quantified formulas contained in K and F.
3. This is an instance of some quantifier consequence wich give true conclusions in every domain.
4. This is derived by applying substitution rules from known equalities and equivalences.

In the first way, we can decompose a proof in a modular way into a number of smaller proofs or reuse the knowledge represented by previously proved propositions. The other ways are explained in the following subsections.