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
