Hi Bill, | svn checkout http://hol-light.googlecode.com/svn/trunk/ hol_light | [...] | Checked out revision 135. | (poisson)richter> du -s hol_light/ | 47772 hol_light/ | I see you added Freek's miz3, and hol.ml still reads | let hol_version = "2.20++";; | (poisson)richter> tar zcvf HOL-L135.tar.gz hol_light | (poisson)richter> du -s HOL-L135.tar.gz | 7372 HOL-L135.tar.gz
That looks fine. I think every version or revision of HOL after 2.20 has just been called 2.20++. I should probably start labelling them in a more discerning way. | mew (woodcock), all mathematicians accept is that math is nothing but | corollaries of the ZFC set theory axioms in a model of ZFC, which is | presumed to exist. That is, we use the set theory axioms on sets that | we assume actually exist. In practice, mathematicians don't | understand ZFC very well, and Halmos's book Naive Set Theory explains | how hard it is to get the real line out of ZFC. Yes, I think there is a striking difference between how mathematicians think about proofs in practice and the widespread assumption that they can "in principle" be formalized in set theory. The following talk I gave a while ago talks a bit about this distinction, among other things. http://www.cl.cam.ac.uk/~jrh13/slides/principia-27nov10/slides.pdf | I'm sure John understands ZFC better than I do, and I assume he | coded the ZFC axioms in some first order logic way in HOL LIGHT. | And I assert that no mathematician would quarrel with John's HOL | LIGHT formulation of ZFC. Actually the HOL Light set theory is built basically by just adding the axiom of infinity to the core higher-order logic, treating sets over a type A as predicates on A, i.e. functions of type A->bool. The resulting set-theoretic universe has a more "typed" character, and it can be interpreted in a fairly straightforward way inside ZFC. If you ignore complications from polymorphism, all the types you can talk about in HOL naturally live in V_{omega+omega} in the Zermelo hierarchy because you can only use the function space constructor finitely many times starting with some infinite type, which you could assume countable. | Now the ZFC model proofs that mathematicians create are much nicer to | read than FOL proofs, but set theorists proved that such ZFC FOL | proofs must exist. The theorem (I forget what it's called) is that if | a theorem is true in every model of a first order theory, then there | exists an axiomatic FOL proof of the theorem. This is usually just called the "completeness theorem" for first-order logic and, at least in this explicit form, is generally attributed to Goedel. If you abstract from the details of a particular first-order proof system, you might say that the essential content is that the set of FOL-provable formulas is recursively enumerable (semicomputable). In that form you can also find it implicit in work of other logicians like Skolem and Herbrand, even if the concept of an r.e. set was not clear at the time. John. ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
