[isabelle-dev] Isabelle/HOL axiom ext is redundant
lp15 at cam.ac.uk
Thu Nov 12 10:12:00 CET 2009
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.
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.
More information about the isabelle-dev