   Go backward to B.4 Decomposing the GoalGo up to B Proving PropositionsGo forward to B.6 Example ## B.5 Deriving New Knowledge

At some point (at least if the goal is an atomic formula with a predicate of the underlying theory), we have to start to operate with the available knowledge in order to derive a situation in which the goal is part of the knowledge.

Proposition 149 (Proof by Case Distinction) For proving with knowledge K the goal G, it suffices to prove G with additional knowledge F and to prove G with additional knowledge ~F (for some formula F).
 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 (F0 \/ ... \/ ...Fn-1) in our knowledge:

 K union {F0 \/ ... \/ Fn-1} G
~~>
 K union {F0} G
...
 K union {Fn-1} G
which is indicated as
We have to prove G. Since we know (F0 \/ ... \/ Fn-1), it suffices to consider the following cases:
• Case F0: ...(proof of G with additional knowledge F0).
• ...
• Case Fn-1: ...(proof of G with additional knowledge Fn-1).

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

Proposition 150 (Universal Quantification in Knowledge) For proving with knowledge K union {forall x: F} the goal G, it suffices to prove G with additional knowledge F[x <- T] for any term T:
 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.

Proposition 151 (Existential Quantification in Knowledge) For proving with knowledge K union {exists x: F} the goal G, it suffices to prove G with additional knowledge F[x <- a] for some object constant a that does not appear in K, G, or F:
 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.

Proposition 152 (Additional Knowledge) For proving with knowledge K the goal G, it suffices to prove G with additional knowledge F, if F holds in every domain in which (some of) the formulas in K holds.
 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
(respectively
 S F
for some S subset K):
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.

• B.5.1 Propositional Consequences
• B.5.2 Quantifier Consequences
• B.5.3 Substitutions

• Author: Wolfgang Schreiner
Last Modification: October 4, 1999   