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

[Brian Huffman]

On Wed, Nov 11, 2009 at 1:46 PM, Alexander Krauss <krauss at in.tum.de> wrote:
> in essence, ext and subst etc. are the real axioms, and eq_reflection is
> an admissible rule which exists for technical reasons, but not a first-class
> citizen.

So eq_reflection is an axiom, but we all agree to pretend it's not an
axiom? This is just weird.

> While we're discussing it: I wonder sometimes what the role of == was in
> earlier days of Isabelle. When viewing Pure as the natural deduction
> framework to encode my logic, I usually interpret ==> as the "is derivable
> from" relation, and !!x as the "this derivation can be done uniformly for
> all x". But I have no such clear idea about ==. Rather I have the feeling
> that with extensionality, == is quite strong compared to this... Was it
> always like this? Or has the simplifier anything to do with this story?

If eq_reflection were not declared as an axiom, then I think it would
make sense to interpret (==) as beta-eta-delta convertibility (where
"delta" conversions involve unfolding constant definitions). Since
(==) is extensional, the convertibility relation would necessarily
include reductions under lambdas as well.

(Actually, it is slightly more complicated than that, since there is a
primitive inference rule Thm.equal_intr that makes (==) at type prop
the same as bi-implication. I don't really see why equal_intr needs to
exist at all; maybe just to make simplification easier? Oh, well.)

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.

- Brian