[isabelle-dev] Isabelle/HOL axiom ext is redundant
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Fri Nov 13 10:25:42 CET 2009
Am 13.11.2009 um 10:07 schrieb Lawrence Paulson:
> 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?
I'm not sure this is the right analogy; after all, your retorical
question, in the original context of !! and ==>, can be answered by
"the HOL4 and HOL Light developers." Isabelle's metalogic, just like
and/or/not/implies, is extracting a certain price, and some of the
people paying that price are wondering what they get for their money.
If nothing else, this discussion was very informative.
More information about the isabelle-dev