Go backward to B.4 Decomposing the GoalGo up to B Proving PropositionsGo forward to B.6 Example |

~~>

KG

Kunion {F}G

Kunion {~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 proveG.

- Assume
F. Then ...(proof ofGwith additional knowledgeF).- Assume ~
F. Then ...(proof ofGwith additional knowledge ~F).

Frequently a case distinction is introduced in situations where we have a
formula (`F`_{0} \/ ... \/ ...`F`_{n-1}) in our
knowledge:

which is indicated as~~>

Kunion {F_{0}\/ ... \/F_{n-1}}G...

Kunion {F_{0}}G

Kunion {F_{n-1}}G

We have to proveG. Since we know (F_{0}\/ ... \/F_{n-1}), it suffices to consider the following cases:

- Case
F_{0}: ...(proof ofGwith additional knowledgeF_{0}).- ...
- Case
F_{n-1}: ...(proof ofGwith additional knowledgeF_{n-1}).

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

~~>

Kunion {forallx:F}G

Kunion {forallx: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 proveG. Since we know (forallx:F), we haveF[x<-T] and thus ...(proof ofGwith additional knowledgeF[x<-T]).

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

~~>

Kunion {existsx:F}G(

Kunion {existsx:F,F[x<-a]}Ganot inKunion {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 proveG. Since we know (existsx:F), we have have someawithF[x<-a]. Thus ...(proof ofGwith additional knowledgeF[x<-a] for some new constanta).

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.

~~>

KG(

KunionFGFholds in every domain in whichKholds).

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

(respectively

KF

S |

F |

- This has been shown in a previous proof or is shown as a subproof.
- 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`. - This is an instance of some
*quantifier consequence*wich give true conclusions in every domain. - 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.

Author: Wolfgang Schreiner

Last Modification: October 4, 1999