On 30/08/2012, at 17:58, Bill Richter <[email protected]> wrote:
> 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). Of course, I meant "mechanical theorem-proving in a system such as HOL Light" when I wrote "theorem-proving". Your ability to prove theorems in the traditional sense is what I meant to imply by describing you as mathematically sophisticated. > 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. Freek intentionally set the default limit to 1, knowing full well that it would limit the ability of the theorem prover to make inference leaps. If he'd wanted the default to be -1, he could have made it thus. The beer bottle analogy is bogus because Heineken can't ship their bottles already open. Freek, on the other hand, could ship miz3 with a default of -1 if he wanted to. Perhaps he now will because of this very discussion... Put it another way: out of the box, the system makes smaller inference leaps than it might otherwise because of an explicit decision by an informed system designer. That is intentional shackling. And really, why do we care? If you want think of HOL Light + miz3 as an unshackled dove, that's your privilege. I will not stir the pot any further. > 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. The set theory you do in HOL is not so far from set theory in traditional ZFC. When you assert your type of point, you say that what follows is all going to happen with respect to an unspecified non-empty set that you're calling "point". When you write x : point you can read this as either "x has type point" (the HOL reading) or "x is an element of the set point" (the reading we can derive using the semantics) When you write UNION : (point -> bool) -> (point -> bool) -> (point -> bool) you are referring to the function which constructs the "or" of two predicates over elements of the set point. Because predicates over points can be freely seen as subsets of the set point, this maps exactly to the traditional ZFC union constant. Everything you do in HOL can be seen as a ZFC construction that has been bounded above by various non-empty sets. > 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. In my experience, getting PAs to do maths is generally much more fun than getting them to do software verification. People often characterise verification work as shallow but broad, where broad really just means tedious in the computer, and unimaginably tedious with pen and paper. Who wouldn't rather be doing deep stuff? Best, Michael ------------------------------------------------------------------------------ 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
