[isabelle-dev] Isabelle/HOL axiom ext is redundant
schropp at in.tum.de
Thu Nov 12 23:06:13 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
But we can prove all instances of the eq_reflection propagation theorem,
> 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? ^^
More information about the isabelle-dev