foundation
slawekk
screenshots from the slides show Isabelle/HOL, but there is also some
mention about importing IsarMathLib, which is Isabelle/ZF . So, will
it be type or set theory ?
I personally vote for the ZF set theory.
Slawekk
Cameron Freer
I also vote for ZF set theory. That screenshot is not really
representative -- it was just a quick example that I thought illustrated
a simple argument that was made even more transparent in the formalization.
I've talked a bit with some of the Isabelle developers about different
ways of importing Isabelle/HOL (and even HOL Light or HOL4) results
into Isabelle/ZF, but I entirely agree with you that Isabelle/ZF (in a
human-readable Isar style) is the correct basic choice.
It would be nice to eventually figure out how to make those aspects
of mathematics which are more easily done in HOL
(as Paulson has recently mentioned:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2008-September/msg00039.html )
equally easy in ZF. Perhaps locales or other methods of abstracting away
the low-level defintions may be useful here.
It's also unclear to me to what extent Isabelle/HOL is an easier
setting in which to do certain sorts of math due to the type theory
vs. just a larger existing body of results. The latter will naturally
improve over time, but it's worth seeing how we might mitigate the former.
Best,
- Cameron
slawekk
> importing Isabelle/HOL (and even HOL Light or HOL4) results
> into Isabelle/ZF,
emulation of the standard mathematics based on set theory. You can see
for example in the Isabelle's Group.thy theory file what happens when
you try to emulate that emulation back in ZF.
The standard definition of a monoid (as found for example at
http://en.wikipedia.org/wiki/Monoid) is that it is a set with a binary
operation (which is another set) that satisfiy certain conditions.
Isabelle's Group.thy on the other hand defines it as a locale, that
has a "struct" in it and makes certain assumptions on the behaviour of
some meta-functions that they define above. As the comments explain
all that is done to simulate "records". I guess they would be happier
if they could just use records, but since this is ZF they have to
simulate them. Look also at the use of the keyword "definition" . They
define a couple of meta-functions that they then use in the locale
assumptions to actually define the concept of monoid. This is
"definition" of behaviour meant as in programming, like say in C you
have got definitions and declarations, not definition as understood in
mathematics.
I think if you set up the right tools for growth, in a couple of years
the initial size of the library will not matter. Wrong definitions
however can hurt the project in the longer term.
Slawekk
Hendrik Boom
theory would work, but it doesn't have to be type theory. If we could
keep track of which theorems are constructive and which not, that
could be a start.
(2) I haven't seen any really foundational category theory. Is there
any? Sure, I can understand you can have objects and arrows, and
build lots of stuff with them, but then they start working with sets
of arrows, and the category Set, and so forth. Does this mean that
set theory is an inherent contaminant in category theory?
(3) Would it be possible to modularize -- separate the logic and
axioms from the rest of the system, so that it would be easy to plug
in others? Or have several, and keep track of what ea proved with
what axioms, with what logics?
slawekk
> any?
(Isabelle/HOL).
Freek Wiedijk compares some foundations in [Is ZF a hack](http://
www.cs.ru.nl/~freek/zfc-etc/zfc-etc.pdf).
Category theory is one of them. This is apparently based on some e-
mails and FOM posts. It is indeed a strange situation. Is category
theory a string theory of mathematics?
>(3) Would it be possible to modularize -- separate the logic and
> axioms from the rest of the system
technically there would be no problem with having a common wiki that
manages development trees based on different foundations. Of course
things that I don't have to do are always easier than those that I am
doing, so I may be underestimating the effort.