[isabelle-dev] Isabelle/HOL axiom ext is redundant
brianh at cs.pdx.edu
Thu Nov 12 00:22:27 CET 2009
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
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.
More information about the isabelle-dev