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

[Michael Norrish]

Makarius wrote:
> On Thu, 12 Nov 2009, Lucas Dixon wrote:

>> this is interesting to me: I don't understand why you couldn't just
>> use the --> and ALL of HOL to do exactly what ==> and !! are doing?
>> Isn't that what SPL by Zammit did? The dependencies (in Isabelle,
>> stored in hyps) can all be recorded outside the logic (as they are in
>> SPL). If done correctly, like Isar, the final theorems can be
>> re-constructed easily enough from the recorded structure of the proof
>> text... or so it seems to me. :)

> The hyps are not involved at this point.  This is about what I've called
> "the visible part of ND reasoning" before.  The nice thing of explicitly
> outlined ND rules via ==> and !! is that the system knows how to combine
> them from their shape.  It is not about "two versions" of certain
> connectives, but a ND rule calculus that is used together with a fully
> featured object-logic.

Because, as discussed, the notions correspond in HOL, one could
emulate ND by defining new constants equal to the existing object
logic implication and universal quantification.  One would then prove
the ND rules in terms of these.  As Makarius said, one would then also
have to "reinvent" the implementation of things like resolution over
these connectives in order to get that nice uniformity that Isaballe
already has.

Of course, I also believe that one might emulate this nice uniformity
in theorems and reasoning by writing sufficiently clever ML code
(which would be parameterised by appropriate theorems, say).  When the
logic reaches its limits (for example, in the construction of
algebraic datatypes we can't express the idea of type existence as a
theorem), this is the last recourse that all the HOL systems must
stoop to.

Michael.