A Structured Proof Format
This section describes a simple structured format for presenting proofs.
The basic ideas are due to Ralph Back and Joakim von Wright,
and a more complete description is being prepared by the three of
us (Back, Grundy and von Wright 1996).
The structured nature of the format allows proofs presented in it to be
browsed at varying degrees of detail.
By way of introduction, consider the proof below.
The problem, to prove that k3 + k is even,
was part of the 1955 Finnish high-school general mathematics
matriculation exam.
|
= |
{Extract the common factor.} |
|
= |
{Distribute even over ·.} |
|
= |
{Since even(i + 1) is
¬(even i).} |
|
= |
{The definition of square.} |
|
= |
{Distribute even over ·.} |
|
|
even k \/
¬(even k \/ even k) |
|
= |
{Disjunction is idempotent.} |
|
= |
{Law of the excluded middle.} |
The format this proof is presented in is known as
calculational proof
(Gries and Schneider 1993)
and is popular among computer scientists.
It is also quite similar to the way in which a high-school mathematics
student might present it, except perhaps for the descriptive comments.
The popularity of this proof format can be explained by its readability
and uniformity.
One drawback of calculational proof is that there is no way to decompose
a large proof into smaller ones.
Large arguments are usually presented semi-formally as a collection of
calculational proofs stitched together with informal text.
Natural deduction (Gentzen 1935),
another common proof method, is particularly good at decomposing large
proofs into smaller ones.
However, natural deduction proofs are seldom as easy to read as
calculational ones.
Can we invent a proof format that combines the structuring facilities of
natural deduction with the readability of calculational proof?
The proof just presented is not large enough to require structuring;
nevertheless, it can be used to demonstrate the concept.
Steps 3-6 of the proof transform the same subexpression,
the right disjunct.
It can be advantageous to think about these steps as a single separate
subproof which transforms even(k2 + 1) into
¬(even k).
Using the structured calculational proof format of Back, Grundy and
von Wright (1996),
we can re-express the proof to make the separate subproof explicit.
|
= |
{Extract the common factor.} |
|
= |
{Distribute even over ·.} |
|
|
even k \/
 even(k2 + 1)
|
|
= |
{Simplify the right disjunct.} |
 |
even(k2 + 1) |
|
= |
{Since even(i + 1) is ¬(even i).} |
|
= |
{The definition of square.} |
|
= |
{Distribute even over ·.} |
|
= |
{Disjunction is idempotent.} |
|
|
even k \/  ¬(even k)
|
|
= |
{The law of the excluded middle.} |
Note that we marked the right disjunct like this
before the
subproof, and like this
afterwards.
The marking is intended to show the reader which part of the
expression is transformed by the subproof.
The basic structuring step of the format is to identify a subterm of the
larger term to be transformed,
and separate off its transformation into a nested subproof.
The example has just one nested subproof,
but in general there may be proofs within proofs, and so on.
When we remove a term from its context, we loose information.
For example, the term even x is not as meaningful in
isolation as it is in a context like
(x = 2) => (even x).
To counter this drawback, we extend the format by allowing a subproof to
begin with a list of assumptions (enclosed in angled brackets) that
follow from its context.
These assumptions, and those of any enclosing proofs,
may be used throughout the subproof.
For example, using the format we can simplify
(x = 2) => (even x) as follows:
|
|
(x = 2) => (even x)
|
|
= |
{Simplify the consequent.} |
|
|
<x = 2> |
|
|
(x = 2) => T
|
Quantification places restrictions on the inheritance of assumptions,
but we need not discuss that here.
A Browsable Format for Proof Presentation: A Structured Proof Format /
Jim Grundy