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

Alexander Krauss krauss at in.tum.de
Wed Nov 11 22:46:38 CET 2009

```Hi Brian,

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

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

http://isabelle.in.tum.de/repos/isabelle/rev/b0b30fd6c264

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?

Alex

```