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

[Makarius]

> On 11 Nov 2009, at 23:22, Brian Huffman wrote:
>
> Anyway, since eq_reflection actually *is* an axiom, and (=) actually 
> *does* mean the same thing as (==), then I really don't see any reason 
> why we need to have both (or separate bool and prop types, for that 
> matter). I don't know of any other HOL provers that do.
> 
> Even if we got rid of the bool/prop and (=)/(==) distinctions, we still 
> have the "meta-meta-logic" as a natural deduction framework: The "hyps" 
> component of theorems encodes the "is derivable from" relation, and free 
> variables in theorems encode the "this derivation can be done uniformly 
> for all x" property. I have never understood why Isabelle needs multiple 
> levels of meta-logics.

It does not "need" to have it, but Larry was visionary enough to provide 
all this from early on, even though it could be considered a bit redundant 
in 1989.  Around 1999 we discovered many ways to make proper use of the 
extra levels, both for the Isar proof language and a very early version of 
locales.  In 2009 it is no longer conceivable to be without the concept of 
"fixes" / "asssumes" in the background context (cf. the more recent local 
theory concept, that allows to do definitional specifications with 
Hindley-Milner polymorphism relative to an axiomatic theory).

While fixes/assumes (cf. "hyps") are there in the background, the visible 
part of ND reasoning works via Larry's great rule calculus for !! and ==> 
which is based on the "resolution" and "assumption" primitives.  These are 
so important to be part of the inference kernel, even though they could be 
derived.


Back to "==" in Pure:  I recall Larry stating "== expresses definitions" 
in some very early Isabelle manual.  Later the Simplifier started to use 
it for convenience and efficiency.  Moreover, derived definitional 
packages were becoming more common, where the "equational 
characterizations" where stated via object-logic equality, and results are 
derived from the Pure definitions as theorems.  Nowadays, even 
'definition' is such a derived mechanisms, and there is little reason left 
to use "==" in user theories (although some people seem to prefer the 
syntactic priority of the == notation).

So I'd say, "==" is a formal device of Pure both for foundational reasons 
and to help building tools (not just the Simplifier).


On Thu, 12 Nov 2009, Lawrence Paulson wrote:

> If you do these things, you put an end to all Isabelle logics other than 
> Isabelle/HOL. Remember, an object logic does not need to possess an 
> equality symbol or even an implication symbol.
>
> Having just translated some lengthy, incomprehensible HOL proofs into 
> Isabelle, I appreciate more than ever the distinction between the meta- 
> and object- levels. HOL proofs are cluttered with extra steps to 
> manipulate implications because HOL has no other way to express the 
> dependence of a fact upon conditions.

Yes, even though HOL could be amalgated into Pure, one would loose the 
declarative outline of natural deduction rules provided via !! ==> (here 
the bool/prop distinction enforces a clear separation of layers, and 
prevents slightly odd mixture of "rules" inside compact object-level 
statements).  If bool and prop would be collapsed, then Isabelle/HOL would 
really have "two versions of quantification and implication", but now it 
has only one version and the other layer expresses pure ND outlines.

BTW, the mechanism for calculational reasoning in Isar can serve as a 
simple example fto study the benefits of "declarative" ND rules in Pure. 
People have occasionally tried to implement calculational reasoning in 
other systems, but it came out more complicated and less general.


 	Makarius