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. I should try to port your solution to Mizar. Most of what else you said was too advanced for me to respond to, but I'll work on it.
Makarius, I (following Freek) tend to think that Isabelle might be the best language for high school teaching axiomatic proofs, but Isabelle is intimidating, lots of programs to install & lots of dox. If you could start porting my Mizar code so I could see the pattern.... 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). 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''. Cris, thanks for sending me the link of new_axiom, which I misread. I see now that reference.pdf clearly says that `new_axiom' should only be used basically to add in new axioms to ZFC, such as large cardinals. But `new_definition' looks fine: Evaluating `new_definition' ‘c v_1 ... v_n = t‘ where c is a variable [...] returns the theorem: |- !x_1 ... x_m. c v_1 ... v_n = t That looks like an axiom to me. 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. 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. 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. 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. Roger, thanks for the code. Hartshorne explains this I do not have the impression that Hilbert was thinking much of Euclid's elements I read much of Greenberg's book with no idea whatsoever why Hilbert came up with his axioms, but after reading Hartshorne's book, the light went on: Hilbert was fixing Euclid! I think this is well-known. Hilbert made a lot more sense after I realized that. Hartshorne's book is great anyway, and I fixed some proofs of his in my paper. http://www.math.northwestern.edu/~richter/hilbert.pdf or had any particular interest in improving on its rigour. I'm sure that's wrong, but this probably isn't the place to discuss it. Read Greenberg, who explain that Euclid's angle-addition errors weren't found until they discovered non-Euclidean geometry. Indeed, from the point of view of rigour it takes some forward and some backward steps. I don't know what you mean by backward steps. Greenberg & Hartshorne don't mention any. -- 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
