[isabelle-dev] Explanation required

[Brian Huffman]

Hi Christian,

Please see this thread from isabelle-dev, November 2009:

https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2009-November/000713.html

To summarize: A theorem meta_ext (like ext but using meta-equality
"==" instead of "=") is derivable using only theorem operations of
Isabelle's proof kernel; this is what it means to say that
extensionality is built into the meta-logic.

Axiom ext is actually derivable from meta_ext, but only by using axiom
eq_reflection, which is labeled as an "admissible axiom". (I guess
that means that it is not one of the usual axioms of HOL, but that
adding it as an axiom is somehow conservative, in that it doesn't
extend the set of provable object-level formulas in HOL. I'm not
exactly sure about that, though.)

axiomatization where
  eq_reflection: "x = y ==> x == y" (*admissible axiom*)

- Brian


On Fri, Feb 17, 2012 at 3:46 AM, Christian Sternagel
<c-sterna at jaist.ac.jp> wrote:
> Dear all,
>
> please forgive my annoying questioning. Could anybody elaborate on the
> following comment (to be found in HOL.thy):
>
>  ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
>  -- {*Extensionality is built into the meta-logic, and this rule
>       expresses a related property.  It is an eta-expanded version
>       of the traditional rule, and similar to the ABS rule of HOL*}
>
> How is extensionality already part of the meta-logic (and how could it be
> applied, e.g., in Isabelle/ML)? And why is "ext" needed? Shouldn't this be
> derivable if we have extensionality?
>
> I know that I read about this in some HOL book, but I forgot in which one.
> Maybe someone could clarify also the following:
>
> For me, extensionality in the meta-logic would be something like "(!!x. f x
> == g x) ==> f == g", i.e., (almost) the eta-contracted variant of "ext"
> above. Is the eta-expanded version (i.e., ext) merely convenient or really
> needed?
>
> cheers
>
> chris
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev