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

[Lawrence Paulson]

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.
Larry

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?