On 5 Aug 2012, at 08:18, Bill Richter wrote: > Thanks, Ramana! I've often wanted Isabelle locales. Are you going to code > them in HOL4?
Locales are one of the many things that (I believe) make the Isabelle HOL logic much more bloated than the original and best HOL logic as supported by HOL4, HOL Light, HOL Zero and ProofPower. It might be possible to give a similar facility as a bolt-on outside the logic. > 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 > People who don't know about Voevodsky's ideas may like to watch the videos of two interesting talks by him: http://video.ias.edu/voevodsky-80th http://video.ias.edu/conversations/voevodsky#attachments > 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? That's a very long story. HOL4 and ProofPower came first in the early 90s as a result of roughly simultaneous efforts in academia (HOL4) and industry (ProofPower) to port Mike Gordon's original Classic HOL onto Standard ML. John wrote HOL Light a few years later, see http://www.cl.cam.ac.uk/~jrh13/papers/holright.html for some of his motivation. Holzero is much more recent work by Mark Adams and Mark's website explains his rationale. There is also HOL Omega by Peter Homeier, which is an extension of HOL4 to support quantification over types. > Why don't you all work on the same program? My reason for sticking with ProofPower is that I know it and that, until recently, it was the only HOL that offered civilised logical and mathematical notation (foralls and exists and cups and caps etc.) on screen. ProofPower also encourages you to make nice LaTeX documents out of your specifications and proofs. > 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? > I don't see it like that. I would say that HOL4 is better documented than HOL Light and has a lot more library support for system verification. That said, HOL Light is much better documented now than it was in the past. HOL4 is probably the system of choice for people doing research in hardware or software verification, while HOL Light has got a lot more support for mathematics. > 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. > Actually, in HOL you are working in a model of Zermelo set theory with choice, not ZFC - there is nothing equivalent to the axiom of replacement in HOL. I agree that saying that we work in polymorphic typed set theory gives a better idea of the actual mathematical experience than saying it is higher-order logic. > 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 would say it is because the community has put far more effort into tools that make it easier to find proofs and because proof automation conflicts with the desire for proof scripts that are readable on their own. For many of us, a long-term goal is to provide tools that can outstrip human capability on useful classes of problems. We can already do this in some cases, e.g., calculating derivatives. If the tool can calculate something for me, why should I have to write down the result of the calculation? Readability of a proof on its own rather than comprehensibility of the proof when you replay it and see what happens is a non-trivial research topic in its own right. I see it as quite problematic. For a start, readability depends on the reader. Very often an expert will be happy with a few strategic pointers while a beginner wants lots of detail, so they need to see different projections of the proof. Personally, I find Mizar proofs unreadable. Or rather I have never learnt how to read them and don't feel greatly motivated to do so. > ... > Thanks, Michael! I think I'll have to learn what polymorphism means before I > can grok your post. In a typed system, polymorphism gives you the ability to formalise a concept like "set union" as a single object "cup" that works for sets of any type, providing the types agree. For example, all the HOLs have distinct types for natural numbers and for real numbers. Without polymorphism, you would need to define distinct functions for all the types you were interested in: nat_cup : nat SET -> nat SET -> nat SET real_cup : real SET -> real SET -> real SET nat_pair_cup (nat x nat) SET -> (nat x nat) SET -> (nat x nat) SET etc. With polymorphism you define: cup : 'a SET -> 'a SET -> 'a SET where "'a" is a so-called type variable. cup then works as if it has every type of the form "t SET -> t SET -> t SET". > 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. You may be interested in my ProofPower development of a little bit of elementary topology. See: http://www.lemma-one.com/ProofPower/examples/wrk067.pdf You will see there how polymorphism can obviate the clunky distinction between classes and sets that one gets when working in first-order set theory. I define a polymorphic set 'a Topology as the set of all topologies with points of type 'a. This is then a first-class object representing the class of all topological spaces. > > 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)? It means that types denote sets and terms denote elements. Each term has a unique type and is guaranteed to denote an element of the set denoted by that type. (When you write down a term in the concrete syntax, you don't have to write down all the type information associated with it. The tool infers a most general possible type for the term and uses that. Abstractly and in the underlying represention used in the tool, all the type information is there in the term.) > And does that mean that U is not the universe of sets, but instead, the > "universe" of types? The denotations of types range over U and the denotations of terms range over \bigcup U. > 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. > The definition of the closure properties required of U finish on the top of the second page! Regards, Rob. ------------------------------------------------------------------------------ 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
