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

[Steven Obua]

>
>
> 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  
learnt ;-)

Steven

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
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20091112/66863895/attachment.html>