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)