5 views

Skip to first unread message

Sep 16, 2008, 5:39:37 PM9/16/08

to vdash

What foundation is planned for the formalized mathematics wiki? The

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

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

Sep 16, 2008, 5:53:41 PM9/16/08

to vdash

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

Sep 17, 2008, 6:04:50 PM9/17/08

to vdash

> 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

Oct 7, 2008, 3:09:57 PM10/7/08

to vdash

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?

Oct 9, 2008, 9:25:02 AM10/9/08

to vdash

> (2) I haven't seen any really foundational category theory. Is there

> any?

Category theory has been formalized inside set theory (Mizar) and HOL
> 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.

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu