[isabelle-dev] Isabelle/HOL axiom ext is redundant
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