On Thu, Nov 12, 2009 at 2:06 PM, Andreas Schropp <schropp at in.tum.de> wrote: >> 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).
This is very interesting... I'd like to learn more about the status of eq_reflection as a meta-theorem. Is there a paper about this? - Brian