[isabelle-dev] Isabelle/HOL axiom ext is redundant
makarius at sketis.net
Thu Nov 12 14:19:19 CET 2009
> 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
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.
More information about the isabelle-dev