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

Makarius makarius at sketis.net
Thu Nov 12 13:43:41 CET 2009

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


More information about the isabelle-dev mailing list