On Thu, Nov 12, 2009 at 1:12 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote: > If you do these things, you put an end to all Isabelle logics other than > Isabelle/HOL. Remember, an object logic does not need to possess an equality > symbol or even an implication symbol.
OK, good point. All the Isabelle logics I have really looked at (HOL, ZF, FOL, LCF) have implication, equality, and an eq_reflection axiom. For these, it might make sense to formalize them by adding operations and axioms about type prop, instead of adding a new type "bool" or "o". But I can see that this wouldn't work so nicely with logics without equalities or implication. > Having just translated some lengthy, incomprehensible HOL proofs into > Isabelle, I appreciate more than ever the distinction between the meta- and > object- levels. HOL proofs are cluttered with extra steps to manipulate > implications because HOL has no other way to express the dependence of a > fact upon conditions. > Larry Right, having two kinds of implication (--> and ==>) is convenient because (==>) is used to encode subgoals with premises in apply-style Isabelle proofs. But this justification for having two implications is completely separate from the one you mentioned above, isn't it? With declarative Isar proofs, I don't think the distinction between --> and ==> is nearly as important, because users don't see so many subgoals encoded with (==>). HOL's problems with manipulating implications would probably be helped by having declarative Isar-style proofs too. - Brian
