[isabelle-dev] Isabelle/HOL axiom ext is redundant
obua at in.tum.de
Thu Nov 12 00:33:56 CET 2009
> Anyway, since eq_reflection actually *is* an axiom, and (=) actually
> *does* mean the same thing as (==), then I really don't see any reason
> why we need to have both (or separate bool and prop types, for that
> matter). I don't know of any other HOL provers that do.
> Even if we got rid of the bool/prop and (=)/(==) distinctions, we
> still have the "meta-meta-logic" as a natural deduction framework: The
> "hyps" component of theorems encodes the "is derivable from" relation,
> and free variables in theorems encode the "this derivation can be done
> uniformly for all x" property. I have never understood why Isabelle
> needs multiple levels of meta-logics.
I agree, these multiple levels are unfortunate ... But I think it is
too late to change this now, as frameworks like Isar and many other
packages rely on them.
In a new theorem prover built from scratch (but of course based on
many years of Isabelle experience...) this would be one of the lessons
PS: Now that the Google App Engine is here (with support for Java
(that means, also Scala -> Makarius)), wouldn't it be great to make
this new theorem prover a native of the cloud?
> - Brian
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev