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).
~~>
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.
- Assume F. Then ...(proof of G with additional
knowledge F).
- 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 |
~~>
...
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,
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,
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.
~~>
(F holds in every domain in which K holds).
This last rule is a "placeholder" for a number of ways to infer
(respectively
for some S subset K):
- 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