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

[Andreas Schropp]

Makarius wrote:
> 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. 

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

I was under the impression that Pure with animation of meta-inductions 
done in ML (or via fast or something) gives us all observable 
consequences of a real meta-logic. I think thats because the reflection 
principle of ZFC is most commonly thought as a meta-theoretic result, 
but we get all consequences in Isabelle/ZF, is that true?

So is the main thing which distinguishes a "logical framework" from a 
"meta logic" the presence of a formal way to do meta-induction (and not 
only prove all cases) and termination checks etc?

The funny thing is: Twelf as an implementation of a logical framework 
seems to include these things, so is it actually a meta logic and not a 
logical framework? ^^

Regards,
  Andy