Rob, I want to argue that Peter Andrews's book To Truth Through Proof supports
my idea of informal mathematics documentation for HOL Light. I don't
understand yet how the informal math compares to your HOL documentation
http://www.lemma-one.com/ProofPower/specs/spc001.pdf
Mostly I'm going to talk about natural deduction, due to Gentzen, about which
I'm far from an expert http://en.wikipedia.org/wiki/Natural_deduction
Andrews in sec 30 (p 155) defines ``a system N of natural deduction, in which
is it possible to give fairly natural and well-structured proofs.'' N is
needed because standard FOL proofs are ``long, awkward, and unpleasant to
read,'' but N is a convenience and not a new formal framework, and in fact,
``the rules of inference of N are all derived rules of inference of [FOL].''
Surely this means that we use our informal math skills (however we think
they're formalized) to prove informal math theorems about FOL deduction. The
rules of Inference of N are clearly stated in informal math. Andrew's first
two rules of Inference are
Hypothesis Rule (Hyp). Infer H |- A whenever A is a member of H.
Deduction (Ded). From H, A |- B infer H |- A ⇒ B
Here H represents ``a finite (possibly empty) sequence of wffs'', and this H |-
A looks a lot like what we see in HOL Light. Clearly Andrews means that
H |- A is true if there is an FOL deduction of A from the wffs in A,
although I didn't see this written down anyway.
I contend the rules Hyp and Ded are clearly informal math theorem about FOL,
and the terms "infer", "from" and "whenever" are merely odd forms of the usual
informal math usage. It would clearer if Andrews had written
Theorem (Hyp).
Let A be any wff and let H be any sequence of wffs containing A. Then
H |- A is true.
Theorem (Ded).
Let H be any sequence of wffs, and let A and B be any two wffs. Assume that
{A} |- B is true. Then
H |- A ⇒ B is true.
Now one can of course think of natural deduction as a new logical framework,
but if so, we would not know that we were actually proving the FOL theorems
that we set out to prove. So it's better, I contend, to think of Andrew's
system N of natural deduction as informal math theorems that allow us to give
nice proofs of our FOL results. These remarks apply particularly to chapter 5,
which is about a version of FOL that is quite like HOL, in that equality plays
the predominant role. Thus, we ought to write documentation for HOL using
informal math.
--
Best,
Bill
------------------------------------------------------------------------------
Start Your Social Network Today - Download eXo Platform
Build your Enterprise Intranet with eXo Platform Software
Java Based Open Source Intranet - Social, Extensible, Cloud Ready
Get Started Now And Turn Your Intranet Into A Collaboration Platform
http://p.sf.net/sfu/ExoPlatform
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
