[isabelle-dev] Isabelle/HOL axiom ext is redundant

[Brian Huffman]

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