Michael, I detect in your previous post a disturbing definition of theorem-proving:
[Bill] is mathematically sophisticated but a novice as far as theorem-proving is concerned. I think I'm quite good at theorem-proving (I have 11 papers published in Math journals). I'm a novice at formalizing theorems, i.e. using proof assistants to verify a proof or to prove theorems. And even with formal proofs, I've developed some skill at declarative proofs, so I'm really only a novice at procedural formal proofs. I think that's the usual meaning of `theorem-proving' here. Setting that timeout to 1 by default is intentional shackling. So, miz3 is indeed intentionally shackled. No, because `intentional' refers to the mental states of the actor, and `shackling' here means to force the proof assistant to make only small inference leaps. Heineken sells beer bottles that can't be opened by hand. We must ask how Heineken and Freek intend for us to use their products. This isn't a question to settle with objective data such as default timeout values or the fact that you can't (except for those awful twistoffs!) remove the beer bottle top without a special tool. Since Heineken intends for us to use a bottle opener, they're not intentionally shackling their beer bottles, i.e. preventing us from drinking the beer. Since Freek intends for us to raise the timeout (he often posts that -1 means no timeout), he's not intentionally shackling miz3. I wish we were in agreement about theorem-proving and intentional shackles, because I think I'll need a lot of your help to understand your HOL4 Logic manual, which looks perfectly rigorous but I seem to be missing the context. I'm OK until 1.2.2 Semantics of types, where I get befuddled. It sounds like a model M is only defined on type constants, which sounds easy, and somehow forces a definition of M on polymorphic types, and the only type constants I know of are the atomic types bool, ind and the arity-2 operator ->, and the Hilbert choice operator which doesn't isn't relevant to my geometry. So I'm a long way from seeing how to do the set theory I'm used to in HOL. Your manual is a blur to me until 2.3.1 The HOL deductive system, which all looks perfectly fine, but I don't know why it's enough. What I want is just to understand one simple example, HOL in my geometry http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz which is now finished at 4565 lines, and includes a proof without the parallel OppositeSidesCongImpliesParallelogram_THM : thm = |- ∀A B C D. Quadrilateral A B C D ⇒ ∡ A B C ≡ ∡ C D A ∧ ∡ D A B ≡ ∡ B C D ⇒ Parallelogram A B C D Cris wrote something similar to what you wrote about Los's logic result In learning situations I certainly would want to be able to control the power level of a proof assistant. Since you can't prevent students from using a more powerful PA (such as Vampire), you'll have to make rules about what constitutes an acceptable proof in your class. In the math courses I want to teach, my rule would be you have to be able to explain your proof to me. In classes on hardware verification where humans can't understand the proofs with pencil/paper, different rules would be needed. I'm mostly saying that I think such rules show the students more respect than shackling the offical class proof assistant (PA). I think it's a question about aims. Published math papers often rely on calculations performed by computer programs. Mathematicians will no doubt soon be relying on their PA for much more help. I'm not trying to say this is a bad idea. My aim is for folks to learn mathematical proofs that can be done without computer help, as I think it's a valuable mental discipline. I'd recommend to everyone e.g. to understand Hilbert axiomatic geometry without computers. I strongly think that understanding math proofs without computers will make one better at formal proofs, and that using a PA to verify e.g. Hilbert geometry vastly increases one's pleasure and understanding of the "paper/pencil" math. I imagine most folks using PAs have much more practical aims, e.g. debugging software. I'm really hoping to learn how to debug software with a PA as well. -- 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
