Thanks, Ramana! I've often wanted Isabelle locales. Are you going to code them in HOL4? For readability I'd like to not "constantly have this annoying TarskiModel hypothesis hanging around," as Michael said, but it would be good to write up a longer version of at least part of my code to show that I can avoid both new_axiom and new_type.
Does you folks know about the Coq work of Vladimir Voevodsky, a mathematician with a Fields medal? http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html Vladimir is even in my subject, homotopy theory, although I don't understand any of his. He says he's working on "new foundations of mathematics", although to my untutored eye, he seems to be formalizing homotopy theory: http://www.math.ias.edu/~vladimir/Foundations_library/toc.html My feeling is that Vladimir's work is a sign that mathematicians and CS folks ought to work together on formal proofs. With this in mind, here are a few dumb questions and points: Why are there so many HOLs, HOL Light, Hol4, Holzero? Why don't you all work on the same program? It kinda seems that HOL4 is the theoreticians and John racks up the theorems. That sounds like a good combination to me! Are you exploring different theoretical possibilities? It sure seems to me that "Working in a Model of ZFC" is more descriptive than HOL. Since working in a model is soooo much more pleasant than strict syntactic FOL proofs, that explains why HOL is more pleasant than FOL, but it doesn't justify the terminology. Maybe I'm missing something. Why are miz3 and Mizar the only proof assistants where one can easily write up human readable proofs? Why can't you write readable declarative proofs in every proof assistant, e.g. HOL4? I'd be happy to port my code to HOL4 or Isabelle if I knew how to write human readable proofs there. Michael seemed to suggest earlier that miz3 was intentionally weakened, and I see no evidence of this. It could be that Mizar is intentionally weak (I've read this is a feature in using Mizar to teach classes), and there are Mizar documents I've been told about, but I really don't care about Mizar. Mizar was a great pioneering effort in human readable proofs, but I don't think Mizar is really part of the formal proofs revolution. Freek's code miz3.ml I think just sets up the format for miz3 code, caching proofs, mixing declarative and procedural, all very impressive hard work, and I've found no bugs. The labor of "by" calculations is done in John's Examples/holby.ml, and it's hard to believe that John would have intentionally weakened his own attempt! I found no evidence of intentionally weakening. Freek, Cris and Rob got me to understand that miz3 is a lot more powerful than I thought. Holby.ml does some simple things and then calls MESON, which has a built-in depth! limit of 50 (I don't know what that means), and MESON only does FOL, not HOL (don't quite get that either). How much weakness do these two facts explain? Could we substitute some other prover for MESON to increase the power of miz3? If someone could look at my 3500 lines of miz3 Hilbert axiomatic geometry code http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz they could maybe explain what MESON isn't doing because it's FOL. My unlearned opinion is that my Hilbert code uses real HOL, because there I use so much sets (from sets.ml), but my Tarksi code http://www.math.northwestern.edu/~richter/TarskiAxiomGeometry.ml only uses FOL, and therefore MESON should do a better job on my Tarski code than my Hilbert code. But this is just wild speculation on my part. From skimming your sources very superficially, it looks as if the Between 'constant' would need to be a parameter of TarskiModel too. Thanks, Michael! I think I'll have to learn what polymorphism means before I can grok your post. There ought to be examples in the HOL dox of how to define common complicated set-theoretic structures that come up in math all the time. In math one just says A Tarski plane in a set T together with subsets Between subset T^3 Equiv subset T^4 satisfying these 11 axioms. A Hilbert plane H is more complicated, because of congruence being defined not on points but subsets of H. How about this? A topological space is a set X together with a subset of P(X) called the open sets of X, satisfying various properties. If you read something saying that there is no empty set, it's meaning that there is no empty type. Thanks, Michael, that helps a lot! I definitely missed that. I'm just on page 1 (actually 9) of your Logic manual: This model is given in terms of a fixed set of sets U, which will be called the universe and which is assumed to have the following properties. Inhab Each element of U is a non-empty set. I would have thought that U here is a "universe", the set of sets that we're going be allowed to use. However, this paragraph begins with The HOL syntax contains syntactic categories of types and terms whose elements are intended to denote respectively certain sets and elements of sets. I guess I can't even read that. Does that say that an element of a type is a set (or element of a set)? And does that mean that U is not the universe of sets, but instead, the "universe" of types? Shows you what you get from just reading the first page! If I read the whole manual, or even the first chapter, I'd probably understand. -- Best, Bill ------------------------------------------------------------------------------ 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
