[isabelle-dev] Explanation required

[Christian Sternagel]

Hi Brian,

thanks a lot for the pointer!

What the comment next to eq_reflection really means, would have been my 
next question ;). Anybody?

cheers

chris

On 02/17/2012 03:58 PM, Brian Huffman wrote:
> 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