Hi Chris, My apologies for carrying on about this, but I care for this subject, sorry.
>At some phases of the moon this sounds attractive to me too. For me too :-) The main problem is that you will get lots of extra proof obligations, so it's _not_ "efficient". You can _hope_ that the automation of your system will take care of them most of the time, though. It seems to work like that for PVS. >But my mother used to say, "Be careful what you wish for, >you just might get it." [...] but if `!x. 1/x = 1/x` >is illegal and `!x. ~(x = 0) ==> 1/x = 1/x` is fine, is >it possible to use the classical propositional calculus >definition of the conditional? Well, as I said, I _don't_ want to change the logic. So the meaning of ==> stays the way it is. It's just that you're not allowed to write some statements sometimes. It is true that in this kind of framework you often get strange behaviors like that D(`A /\ B`) is provable, while D(`B /\ A`) is not. I think it's like this in PVS too. It's like in C where (x != 0 /\ 1/x > 0) cannot crash because of division by zero, while (1/x > 0 /\ x != 0) can. In B they have a version of D where this asymmetry of the definedness conditions is not there, but still you will probably get in other places that two formulas that in the total version of the logic are completely equivalent will be different in the sense that one will be allowed while the other is not. No, your mother probably won't like that. The PVS people apparently don't care so much. I guess your mother is not a PVS user? :-) >That looks to me like a fundamental change in the HOL logic. So the _logic_ will stay exactly the same. That's the whole point! The relevant _models_ of the logic to consider probably will be different though. >For me the idea that: "`A = A` for all boolean terms A" So in the thing that I'm imagining _if_ `A = A` is allowed at all, it certainly will be provable! >Perhaps you might achieve a satisfying result by adding >equality-like relations such as (for the real numbers) >`reallyEqual`, meaning "the arguments have determinate >real values that are equal" So that's the kind of thing you get in partial logics. Which is why I don't like that approach either! You should not be allowed to write `A = B` if A or B is non-denoting. So it should not be meaningful to ask whether the equality holds in such a case. But I don't know. Maybe what I'm hoping for won't work in the HOL case. (It _does_ work in the first order case though! At least, that's what the paper with Jan Zwanenburg claimed to show.) I really should try to get this to be more than just hopes at some point. And now I'll shut up about it :-) Freek ------------------------------------------------------------------------------ Precog is a next-generation analytics platform capable of advanced analytics on semi-structured data. The platform includes APIs for building apps and a phenomenal toolset for data science. Developers can use our toolset for easy data analysis & visualization. Get a free account! http://www2.precog.com/precogplatform/slashdotnewsletter _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
