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

[Brian Huffman]

On Thu, Nov 12, 2009 at 2:06 PM, Andreas Schropp <schropp at in.tum.de> wrote:
>> In a sense, eq_reflection is a meta-thereom, but Pure is not a meta-logic,
>> so it cannot be proven within the system.  Thus we need to add it as an
>> axiom.
>
> But we can prove all instances of the eq_reflection propagation theorem,
> right?
>
>> I would consider this as an "implementation detail", and not worry about
>> it any further.
>>
>> Tools that operate on the level of proof terms can then eliminate
>> eq_reflection, as was pointed out first by Stefan Berghofer some years ago,
>> IIRC.  (I also learned from him that it is better to speak about Pure as
>> "logical framework", and not use term "meta logic" anymore.)
>>
>
> Yeah, Stefan does this in HOL/Tools/rewrite_hol_proof.ML (which was tested
> quite thoroughly since 5e20f9c20086, so also in Isa09).

This is very interesting... I'd like to learn more about the status of
eq_reflection as a meta-theorem. Is there a paper about this?

- Brian