[isabelle-dev] Isabelle/HOL axiom ext is redundant[SEC=UNCLASSIFIED]
lp15 at cam.ac.uk
Mon Nov 16 11:31:39 CET 2009
In the beginning, it was precisely as you describe. Even now, Isabelle/ZF and Isabelle/CTT continue to distinguish metalevel functions (which in ZF would be seen as operators or class functions) from the functions of the formalism. I published and implemented an early formalisation of simple type theory based on similar principles, but it wasn't pleasant to use. Tobias convinced me that a viable implementation of higher-order logic would have to use the built-in type inference mechanism, which Isabelle already possessed. This meant, in particular, allowing type variables as well as ordinary variables in users' formalisations of logic.
On 16 Nov 2009, at 01:21, Dr. Brendan Patrick Mahony wrote:
> Thanks for this interesting and enlightening discussion.
> I have always had an intuitive appreciation of the meta-logic in
> Isabelle. I find it clarifies the both the modeling and proof
> activities profoundly.
> I would be interested also in a discussion of an important place where
> the meta-logic is not distinguished from the object logic in Isabelle/
> HOL, i.e. in the function model. HOL functions are completely
> identified with meta-functions (I like to call them operators) and
> there is no explicit function application operator. This makes for
> lots of inconvenience in making proofs about HOL functions, especially
> in the vagaries higher-order unification.
> Any insights in why HOL-application is not as worthy of distinction
> from meta-application as = is from ==? Especially as meta-application
> itself is so subtly identified with term construction?
More information about the isabelle-dev