On 28 Apr 2014, at 00:57, Bill Richter <rich...@math.northwestern.edu> wrote:
> 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.
You are consistently using “informal” where the standard term in the logic
literature is “meta”. What Andrews means is that the rules of inference of N
can be seen by metamathematical reasoning (i.e., by reasoning about the
deductive system, rather than in it) to have the same deductive closure as
(some other system of rules for) FOL.
> 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.
If you replace “true” by “provable”, then this is how one would state Andrews’
claim that the rules of N are admissible in FOL. With “true” rather than
“provable” then what you are stating is the claim that the rules of N are sound
(with respect to some semantics that you need to have in mind to define the
notion of “truth”). This second claim may be “clearer”, but it is not what
Andrews means and the distinction between these two claims is important. It so
happens in FOL that the two claims are equivalent, because with the usual
definition of truth for FOL, Goedel’s completeness theorem for FOL tells us
that truth and provability are equivalent.
>
> 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.
Yes, but there are important distinctions (like the distinction between “truth”
and “provability”) that you need to be careful and precise about in your
informal account.
Regards,
Rob.
------------------------------------------------------------------------------
"Accelerate Dev Cycles with Automated Cross-Browser Testing - For FREE
Instantly run your Selenium tests across 300+ browser/OS combos. Get
unparalleled scalability from the best Selenium testing platform available.
Simple to use. Nothing to install. Get started now for free."
http://p.sf.net/sfu/SauceLabs
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
