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

[Lucas Dixon]

I was really wondering what the principle was that makes "-->" and "ALL"
fail (or be inappropriately convoluted) than using the meta-level
connectives: is there a small example that illustrates it?

My own understanding was that the meta-level of Isabelle, and the use of
it by Isar, facilitated the genericity natural deduction-style
reasoning. Generic proof tools can be written that work across logics.

Makarius, if I understood correctly, was saying that these meta-level
logical mechanisms have a utility even when just within one logic, but I
didn't understand what this would be, except perhaps distinguishing
between ND syntax and other logical syntax (which is my interpretation
of Michael's reply).

best,
lucas

Lawrence Paulson wrote:
> This sort of discussion is analogous to suggesting that we get rid of
> and/or/not/implies and write all formulas using the Scheffer stroke
> (NAND), or that Gentzen's sequent calculus should be replaced by the
> much simpler Hilbert system. It can be done, but who would want to do it?
> 
> Larry
> 
> On 12 Nov 2009, at 20:50, 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 University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.