B.2 Preliminaries
The proof of a proposition is always relative to given knowledge. Initially,
this is knowledge that characterizes the considered domain (axioms),
that is derived from a "harmless" extension (definitions), that is
true in any domain (tautologies) or that has been derived by another
proof (propositions). In the course of a proof, new knowledge is
gradually added (assumptions).
A proof situation consists of the available knowledge K (a set of
formulas) and the goal G to be proved (a formula). We represent
such a situation graphically as
and read this as "we (have to) prove G with knowledge K". In a
natural language proof, the knowledge that is available in a particular proof
situation has to be deduced from the context: it consists of the
knowledge at the beginning of the proof extended by all the temporary
definitions and assumptions that were made in the branch of the proof that led
to the current situation.
A proof rule reduces a proof situation to one or more other
situations. We denote this reduction by ~~> and read
~~>
as "in order to prove G0 with knowledge K0 it suffices to
prove G1 with knowledge K1".
A proof is the reduction of the start situation to other situations that are
again reduced to other situations until we have only situations in which
nothing is left to be proved:
The only way to reach a leaf in this proof tree (i.e., to complete a
particular proof branch) is by the following rule.
Proposition 139 (Proof Completion)
For proving with knowledge K union {G} the
goal G, nothing has to be done any more.
~~>
In other words, if the goal is in our "knowledge base", we are done.
Author: Wolfgang Schreiner
Last Modification: October 4, 1999
