Hi Bill. > Roger, if there's ``some cultural aversion to the use of axioms in the > HOL community,'' then maybe HOL isn't the right proof-checker to use > in high school geometry classes. Does anyone think there is a better > proof-checker? My guess is that this is just an interface problem > that HOL could easily solve, and I'm willing to work on it myself. > I'm working on a formalisation of Hilbert's FoG, and am mostly using the Mizar Light mode in HOL Light.
Perhaps controversially, I've used "new_axiom" for every one of Hilbert's axioms. I could have defined a model of Euclidean geometry as John suggests, and obtained the axioms as theorems of the basic HOL logic. However, I wanted to remove the axiom of infinity from the core logic, preferring to derive this from Hilbert's geometric axioms. Without infinity, you're going to be stuck getting a model of Euclidean geometry. Others have mentioned the more modular approach of defining a relation R on variables which stand for Hilbert's various primitive notions. Then a formula such as Group1(on_line, on_plane) can assert that the relations on_line and on_plane satisfy Hilbert's axioms. This would allow you to carry out metatheoretic proofs, at the expense of making all of Hilbert's theorems conditional on Group1(on_line, on_plane). The main issue I then have is that all definitions (and Hilbert needs many just to assert his axioms) need to carry the primitive notions as arguments. I think this would really uglify the proofs, but it should be possible to hide this away with some judicious syntactic sugar, as I believe is done with Isabelle's locales. I'm generally all in favour of teaching rigorous mathematics to high-school students, getting them to use theorem provers and learning to code early. Here in the UK, we are falling ever further behind in terms of computer science at high-school level. That said, it seems that students would be faced with a huge learning curve if they were simultaneously studying a relatively poorly documented language such as Ocaml, a theorem prover such as HOL Light, and the axiomatic method. And my guess is they'll have trouble no matter which theorem prover you pick, though I'm very much interested in your thoughts on how to tackle this. On 26/04/12 05:19, Bill Richter wrote: > Nobody in > my subject buys the proof of the Immersion conjecture > http://en.wikipedia.org/wiki/Whitney_immersion_theorem > Really? That's pretty scary! > 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. It's conservative, though. You won't be able to introduce a contradiction with this function. > 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. What sort of granularity do you want in the proof steps? If you're going all the way to natural deduction, I think the proofs are going to get massive even at the very beginning of Hilbert's geometry. Maybe Tarski's is more suitable. Phil -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ------------------------------------------------------------------------------ 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
