Hi Michael, >[...] >Use standard principle that allows constants to be >"defined" once existence is proved to give yourself the >choice operator. > >Now, if you believe in the way HOL Light implements that >last definitional principle, you'll object that this uses >the choice operator.
:-) Yes, exactly. In HOL Light you don't have that "standard principle" in the kernel, and when I think "HOL", I always think of HOL Light which is the only HOL system I know a bit. >But that's just a convenience for John's implementation. No. If he hadn't implemented things this way, I would have objected to this "definitional principle" for exactly the same "I want my closed terms to unambiguously point into the Platonist universe" reasons too. (By the way, in Mizar you only get that "standard principle" if you have proved _unique_ existence. And _then_ of course I don't have any problems with it anymore.) Another by the way: there's something like a choice operator hidden in the type definitions of HOL Light as well. It's the reason that the part of the system that the source claims is intuitionistic, actually isn't. But with that I don't have Platonistic problems, because I can "fix" what the "abs" functions might be. It still will be a choice that you won't be able to prove in the logic, but at least it will be specific. To say it still differently: Goedel told how to show that a theory is incomplete. But with epsilon and your definitional principle it becomes _obvious_ that the theory is incomplete. I would prefer the theory to be "as complete as possible", and to really need the Goedel theorem to get incompleteness. >In reality we know that it's OK to use such things as >constants because their use could be eliminated through >the CHOOSE principle. But that's a different matter! Then you're local to a proof, and not writing closed terms. I've had this discussion many times with Josef Urban as well, and he also kept giving me this argument :-) But somehow I don't think it fully cuts it. If you don't have the choice operator (and/or its definitional principle equivalent), I think that you cannot define a constant in HOL for which you can prove that it denotes a free ultrafilter. _With_ these things it's easy to define such a constant, but without you can certainly _prove_ that free ultrafilters exist (well, if you have AC), but you cannot _define_ one. You cannot _point_ at one. (This is the main reason I like free ultrafilters so much :-)) So, yes, as you say "it's OK", but I still think there's a difference. I've had this discussion with John Harrison as well. He then pointed out a book about the "epsilon calculus" in which it is proved that any statement that you can prove using the epsilon operator but that doesn't itself contain it, you also can prove without. (That was about first order logic though, I think.) So maybe that's what you mean? Still it doesn't take away my feeling of unease. Josef and John (and you :-)) probably all think I'm just being difficult... Ah well, so be it. Freek ------------------------------------------------------------------------------ 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
