[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 mailing list