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

Lawrence Paulson 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 mailing list