Go backward to B.1 Proof LevelsGo up to B Proving PropositionsGo forward to B.3 General Strategies

## 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

 K G

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

 K0 G0
~~>
 K1 G1

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:

 K G
~~>
 K' G'
~~>
 K'0 G'0
~~>
 K'1 G'1
~~>
 K" G"
~~>
 K"0 G"0
~~>
 K"1 G"1
~~>
 K0
 K1
 K2
 K3
...
 Kn

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.
 K union {G} G
~~>
 K union {G}

In other words, if the goal is in our "knowledge base", we are done.

Author: Wolfgang Schreiner
Last Modification: October 4, 1999