On Thu, 26 Apr 2012, Phil Scott wrote:
> Others have mentioned the more modular approach of defining a relation R
> on variables which stand for Hilbert's various primitive notions. Then a
> formula such as Group1(on_line, on_plane) can assert that the relations
> on_line and on_plane satisfy Hilbert's axioms. This would allow you to
> carry out metatheoretic proofs, at the expense of making all of
> Hilbert's theorems conditional on Group1(on_line, on_plane). The main
> issue I then have is that all definitions (and Hilbert needs many just
> to assert his axioms) need to carry the primitive notions as arguments.
> I think this would really uglify the proofs, but it should be possible
> to hide this away with some judicious syntactic sugar, as I believe is
> done with Isabelle's locales.
If you think of the "axiomatization" as a local context with parameters
and assumptions (based on some predicate definition in the background),
then your subsequent definitions become dependent on that context as
abserved above. The locale context of Isabelle manages exactly that by
some extra-logical infrastructure, and this is a bit more than just
syntactic sugar.
In fact, the modest locale concept of 1999/2002 has been refined and
elaborated many times. Around 2006/2007 we've turned it into so-called
"local theory" infrastructure, where locales, type clases, overloading
etc. are just particular targets, which means contexts that can absorb
definitional specifications. In the other dimension you have
"definitional packages" that live in the local theory space: inductive
sets and predicates, recursive functions, etc. Even what looks like plain
definition or theorem statements in Isabelle are non-trivial local theory
packages, and can thus depend on particular context elements without the
user having to care about it very much.
What is conceptually also important here is that we have introduced a
clear separation between the "foundation" level (actual definitional
primitives) and the "user" view on that. So user theories are no longer
directly exposed to the bare metal of the logic. For exmaple, the
proverbial HOL problem from the other thread by Rob Arthan, which is
called "hidden polymorphism" in Isabelle jargon, is absorbed by the local
theory infrastructure:
definition "unitary = (!x. x = x)"
This correctly defines a polymorphic boolean with an implicit type
dependency in Isabelle/HOL. This works out formally, but it might still
be apt to confusion and surprises when used in practice. (There are rare
situations where this is really required in that form.)
Makarius
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
