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

[Alexander Krauss]

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 
again about a year ago:

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