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

[Lawrence Paulson]

If you do these things, you put an end to all Isabelle logics other  
than Isabelle/HOL. Remember, an object logic does not need to possess  
an equality symbol or even an implication symbol.

Having just translated some lengthy, incomprehensible HOL proofs into  
Isabelle, I appreciate more than ever the distinction between the  
meta- and object- levels. HOL proofs are cluttered with extra steps to  
manipulate implications because HOL has no other way to express the  
dependence of a fact upon conditions.
Larry

On 11 Nov 2009, at 23:22, Brian Huffman wrote:

> 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.