Hi Bill, | John, thanks for writing the code for me, but you only handled I think | my question about showing that the type of Tarski models is nonempty.
That's true, I didn't go into the details of the proofs and how to present them in HOL Light. There are several different approaches one might take, and perhaps seeing what Phil Scott and Lorenzo Mannini have done would be a good starting-point. But if you really get stuck I can try porting some of your stuff when I have a bit of spare time. | I'm gratified folks want to read my paper where I fixed a longstanding | combinatorial error in homotopy theory. It's on my web page | http://www.math.northwestern.edu/~richter/RichterPAMS-Lambda.pdf Maybe | I don't teach at NWU, but I did long ago, and they let me use the | computers so I can write such papers. I called the error a `serious | pedagogical gap', as the results were proved in the literature, but | newcomers might easily leave the subject when told these results were | trivial (their teachers didn't know the combinatorial proofs). This is a nice example: even the question of whether a proof is actually faulty or just leaves a huge "pedagogical gap" that the original author was easily capable of filling is itself ambiguous. | There are much more serious problems. Recently lots of top | conjectures fell: Fermat's Last Theorem, the Poincare conjecture, | Bieberbach's conjecture, the Kervaire invariant conjecture (in my | subject, homotopy theory), and I don't have any confidence in these | proofs. Nobody in my subject buys the proof of the Immersion | conjecture http://en.wikipedia.org/wiki/Whitney_immersion_theorem So | I'm really impressed by Tom Hales for saying, ``I'll show I really | have a proof by using HOL, Coq, Isabelle etc for 20 man years''. Interesting to hear you say that, since many mathematicians seem quite blase' about correctness issues, even with the huge proofs that few people could claim to follow in detail. | |- !x_1 ... x_m. c v_1 ... v_n = t | | That looks like an axiom to me. There are two different approaches to definitions in a system like HOL. One can consider them as "metatheoretic", where the definition is just a kind of user interface convenience with no logical status. HOL Light has only trivial cases of this (like "override_interface") but some other systems like Nuprl have a more elaborate mechanism. The "object-level" way is to actually introduce a new constant or constants and a new axiom asserting the appropriate equivalence. This is the main HOL Light mechanism as supported by "new_definition" etc. So yes, in some sense a definition in HOL Light *is* indeed an axiom. However, by virtue of the limited syntactic form it's a very special case of an axiom. As Phil said, in contrast with an arbitrary axiom a definitional axiom is guaranteed to be a conservative extension. That is, if you can prove any theorem |- phi where the formula phi doesn't involve the new constant, then you could have proved |- phi without making the definition. In particular, this works for phi being `false', so you cannot make the logic inconsistent by adding a definition, whereas you can certainly do so by adding axioms. The primitive definitional form is very restrictive, and some derived definitional principles allow you to make, for example, recursive definitions; under the surface these are derived from the primitive form, so retain the conservativity property. For instance here we define the Collatz function. Note that we are not saying anything about the termination of this pattern of recursion, merely that adding it as a new definition is conservative: define `!n. collatz(n) = if n <= 1 then n else if EVEN(n) then collatz(n DIV 2) else collatz(3 * n + 1)`;; The aversion to arbitrary axioms in HOL probably arose because computer scientists have in the past proposed various axiom systems that have turned out to be inconsistent. If you are formalizing a well-established field of mathematics using standard axiom systems, then you are not very likely to make major conceptual errors setting up your axioms formally. However, even then it's easy to make little slips like forgetting degenerate cases. For example, I have seen an axiomatization of real numbers as complete ordered fields in a prover that stated the supremum property as "every set of reals that is bounded above has a least upper bound". Since this forgets to rule out the empty set, it implies that there is a least real number and so leads to inconsistency when combined with the other axioms. There are various stories about mathematicians who spend their entire PhD research studying axiomatic systems that turn out to be inconsistent, trivial or otherwise degenerate. One I remember is "antimetric spaces" with axioms d(x,y) = 0 <=> x = y, 0 <= d(x,y) and d(x,y) + d(y,z) <= d(x,z). I suspect most or all of these are apocryphal, but it would be interesting to know if there is a real documented example. | My only problem is that I don't know how to write declarative code | in HOL. As I posted, I can't get any any of the mizar modes to | work for me, including Freek's latest miz3.miz. The diversity in approaches to declarative proofs in HOL Light is perhaps a bit unfortunate, though they explore different tradeoffs between syntactic elegance, practical usability, programmability and degree of integration with other proof methods. Actually getting any of them running should not be *too* hard anyway: 1. The original Mizar mode for HOL is still there and you can just load it from inside HOL Light: #use "Examples/mizar.ml";; There is a little example at the end of the file to look at, the Knaster-Tarski fixed point theorem. 2. Freek's "Mizar Light" needs one more step first: go into the Mizarlight directory and do "make" (or maybe to be safe, first "make clean" then "make") but then again you can just load it #use "Mizarlight/make.ml";; This also runs an example, which is somewhat relevant to your interests, setting up a model of projective geometry (the Fano plane) and deriving the duals of the axioms. 3. Freek's miz3 isn't distributed with HOL Light (maybe it should be) but you can download it from http://www.cs.ru.nl/~freek/miz3/miz3.tar.gz After untarring it into a subdirectory "miz3" tar xvfz ~/Downloads/miz3.tar.gz You need to have the Unix library loaded; if you don't already have this, then this works on many platforms: #load "unix.cma";; and then you can just load it #use "miz3/miz3.ml";; following which you can try any of the examples there, e.g. the Robbins conjecture proof: #use "miz3/Samples/robbins.ml";; If you do decide to use one of these frameworks, you might be best advised to follow what Phil and Jacques have done, since they have quite a mature system, where they have nice readable proofs but also integrate programming to deal with some gaps. | But I contend that mizar modes should not be needed. The main thing I | like about Mizar is just that it's declarative and I can break proofs | up into cases and do proofs by contradiction. I agree. In fact, in the original paper I wrote promoting Mizar-like proofs for our LCF community, I emphasized that there is not actually such a deep conceptual difference, and there is almost a 1-to-1 correspondence between Mizar structuring steps and HOL tactics. (I do not use the term "declarative" in this paper, though I was groping for some appropriate word. The procedural/declarative terminology was suggested by Mike Gordon when I presented the work in a talk.) http://www.cl.cam.ac.uk/~jrh13/papers/mizar.html Freek's Mizar modes work hard to achieve a true integration of the declarative and procedural styles. To some extent, you can get the declarativity using traditional tactic scripts if you use a few more intuitive tactics and take more care over labelling of assumptions and referring to them by name. Marco Maggesi has been successfully honing such a style and I am planning to incorporate more of those special tactics into the core. Lorenzo's code may be a good illustration, since he works with Marco, though I haven't seen his proofs yet myself. | We really don't want a powerful theorem prover in high school | geometry! We want the kids to have to write down most of the | steps. And unless I'm really misunderstanding Mizar, Mizar would | not be a good language for the kids to program in. Certainly Mizar would not be the first choice for *programming*, but in some ways it seems to be more accessible precisely because you don't need to be a programmer to do proofs in the system. As Phil said, with HOL you also have the additional barrier from confronting the implementation language, even if you use it in quite superficial ways. While it is empowering to have a full programming language available, it can also be intimidating at first, especially to non-programmers. | Any Mizar experts who want to explain | http://www.math.northwestern.edu/~richter/RichterTarskiMizar.tar | how I'm doing it all wrong, I'd be grateful. I'm not sure that so many real Mizar experts read this mailing list, so you may also want to consider posting to mizar-forum. 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
