# Re: Toward a common syntax for writing proofs

bshults@fireant.ma.utexas.edu
Mon, 18 Mar 96 13:01:13 CST

MAKV wrote:
Another related problem is an explication of the notion "proof".
The usual definition of proof as " a finite sequence of one or more
formulas each of which either is an axiom or is immediatedly inferred
from preceding formulas in the sequence by means of one of the rules
of inference" is unsatisfactory for our goals because:

1) This definition is good for "bottom-up" proofs, but real proofs may
be "top-down", that is, a formula in a top-down proof may be inferred
using also some succeding formulas;

2) A real proof may contain not only formulas but also some definitions;

Maybe for our goals it is better to define a proof as a dag; a formula
and an inference rule are attached to every vertex of the dag;
then various syntaxes for writing proofs could be considered as various
ways of flattenning this dag.

Regarding (2): definitions are often thought of as axioms. When they
are not considered to be axioms, there is a proof in most logics that
their use in a proof is sound.

I want to understand a few things better:

When you say "our purposes" and "our goals" are you talking about the
goals and purposes of the QED project or of the VEDA project or of
something else?

I think you mean QED.

When you say "writing proofs" are you talking about a computer's
internal representation, the computer's output, the proof checker's
input or the way humans write proofs in mathematics.

I think that you are suggesting that the internal representation be a
DAG, then the external representation be more human-readable.

Is there a particular DAG proof procedure you are advocating?
Probably most proof procedures can be construed as constructing a
DAG. There are many proof procedures which are very naturally
so construed.

You may also be arguing that a certain DAG procedure (the one VEDA
uses) is somehow better for internal representation in a QED
implementation than other possibilities.

There are various sound proof procedures. Each is preferable for a
different purpose. My understanding is that the QED project would
like to be able to include several of them. Some proof procedures are
nice because humans can understand them more easily. Other proof
procedures are nice because computers can use them more easily. These
two goals are not always exclusive.

It seems to me that having a variety of proof procedures is
advantageous both internally to the computer and externally in the
presentation. The external proof representation should be
human-readable (although output in non-standard proof form will be
interesting to debuggers).

```--
Benjamin Shults                 Email:  bshults@math.utexas.edu
Department of Mathematics       Phone:  (512) 471-7711 ext. 208
University of Texas at Austin   WWW:    http://www.ma.utexas.edu/users/bshults
Austin, TX  78712   USA         FAX:    (512) 471-9038 (attn: Benjamin Shults)
```