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

[Makarius]

On Wed, 11 Nov 2009, Brian Huffman wrote:

> On Wed, Nov 11, 2009 at 1:46 PM, Alexander Krauss <krauss at in.tum.de> wrote:
>> 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.
>
> So eq_reflection is an axiom, but we all agree to pretend it's not an 
> axiom? This is just weird.

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.  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.)


 	Makarius