[isabelle-dev] Isabelle/HOL axiom ext is redundant
krauss at in.tum.de
Wed Nov 11 22:46:38 CET 2009
> Then I was wondering exactly how this axiom was related to the
> "extensionality built into the meta-logic". After looking into it, I
> discovered that I could actually prove the "ext" axiom as a theorem.
I discovered this curious fact myself last year, while trying to
understand the exact relation between Pure and HOL. In fact,
eq_reflection (plus refl, I think) fully axiomatizes the HOL equality as
"the same as ==", and so the axioms ext and subst can both be derived
However, though more "minimal" in a certain sense, this axiomatization
is a little strange in that it exploits the properties of the meta
language, instead of describing the properties of = directly.
In the translation to ZF which Andy and I am developing, such "strange
proofs" actually caused some weird problems at some point. This, and the
intent to make the axiomatization clearer, were the reasons why "subst",
which had been a theorem for quite some time, was replaced by an axiom
again about a year ago:
So, 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.
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?
More information about the isabelle-dev