Bill,
On 19 Mar 2014, at 07:02, Bill Richter <rich...@math.northwestern.edu> wrote:
> work is. If I understood it, I'm sure I'd say it was elegant mathematics,
> and that it's good we're assuming the weakest possible set of axioms.
Have you looked at Peter Andrews’ book "An Introduction to Mathematical Logic
and Type Theory: To Truth Through Proof”. It is a very good introduction to
simple type theory. I don’t have it to hand, but my recollection is that
Andrews’ system has an even more minimalist set of rules and axioms than HOL
Light.
> RDA> Concerning beta-conversion ... You don’t need anything other than
> RDA> Tom’s 10 rules.
>
> Thanks, Rob. I'll study your proof of BOOL_CASES_AX.
I make no claims to have discovered this. I reverse-engineered it from the HOL
Light proof some time ago. From John’s recent post it is from Diaconescu via
Beeson with some improvements by Mark Adams.
>
> RDA> Note that he doesn’t give a schematic presentation of the last
> RDA> two rules that let you substitute for type and term variables, so
> RDA> they are easy to miss.
>
> Ah, and I had missed it, until I saw it in the HOL4 dox. It strikes me that
> I've often been befuddled writing code in that I don't quite understand what
> the type and term substitution rules actually are. Do you feel you do a
> good job in your dox explaining these matters? ProofPower can't really be
> that different theoretically from HOL4 and HOL Light, right?
ProofPower is no different from HOL4 and HOL Light as regards substitution. The
ProofPower documentation does include a formal specification of the logic and
the proof system, but you would probably do better looking at the HOL4 Logic
Manual, which gives a good account based on work of Andy Pitts that uses
traditional maths notation to define the logic including substitution. The
primitive rules and axioms in HOL4 (and ProofPower) are different from HOL
Light, but prove the same set of theorems.
Regards,
Rob.
------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/13534_NeoTech
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
